WORST_CASE(?,O(n^3)) * Step 1: DependencyPairs WORST_CASE(?,O(n^3)) + Considered Problem: - Strict TRS: 'cklt('EQ()) -> 'false() 'cklt('GT()) -> 'false() 'cklt('LT()) -> 'true() 'compare('0(),'0()) -> 'EQ() 'compare('0(),'neg(y)) -> 'GT() 'compare('0(),'pos(y)) -> 'LT() 'compare('0(),'s(y)) -> 'LT() 'compare('neg(x),'0()) -> 'LT() 'compare('neg(x),'neg(y)) -> 'compare(y,x) 'compare('neg(x),'pos(y)) -> 'LT() 'compare('pos(x),'0()) -> 'GT() 'compare('pos(x),'neg(y)) -> 'GT() 'compare('pos(x),'pos(y)) -> 'compare(x,y) 'compare('s(x),'0()) -> 'GT() 'compare('s(x),'s(y)) -> 'compare(x,y) 'less(x,y) -> 'cklt('compare(x,y)) append(l1,l2) -> append'1(l1,l2) append'1(dd(x,xs),l2) -> dd(x,append(xs,l2)) append'1(nil(),l2) -> l2 flatten(t) -> flatten'1(t) flatten'1(leaf()) -> nil() flatten'1(node(l,t1,t2)) -> append(l,append(flatten(t1),flatten(t2))) flattensort(t) -> insertionsort(flatten(t)) insert(x,l) -> insert'1(l,x) insert'1(dd(y,ys),x) -> insert'2('less(y,x),x,y,ys) insert'1(nil(),x) -> dd(x,nil()) insert'2('false(),x,y,ys) -> dd(x,dd(y,ys)) insert'2('true(),x,y,ys) -> dd(y,insert(x,ys)) insertionsort(l) -> insertionsort'1(l) insertionsort'1(dd(x,xs)) -> insert(x,insertionsort(xs)) insertionsort'1(nil()) -> nil() - Signature: {'cklt/1,'compare/2,'less/2,append/2,append'1/2,flatten/1,flatten'1/1,flattensort/1,insert/2,insert'1/2 ,insert'2/4,insertionsort/1,insertionsort'1/1} / {'0/0,'EQ/0,'GT/0,'LT/0,'false/0,'neg/1,'pos/1,'s/1,'true/0 ,dd/2,leaf/0,nil/0,node/3} - Obligation: innermost runtime complexity wrt. defined symbols {'cklt,'compare,'less,append,append'1,flatten,flatten'1 ,flattensort,insert,insert'1,insert'2,insertionsort,insertionsort'1} and constructors {'0,'EQ,'GT,'LT,'false ,'neg,'pos,'s,'true,dd,leaf,nil,node} + Applied Processor: DependencyPairs {dpKind_ = DT} + Details: We add the following dependency tuples: Strict DPs 'cklt#('EQ()) -> c_1() 'cklt#('GT()) -> c_2() 'cklt#('LT()) -> c_3() 'compare#('0(),'0()) -> c_4() 'compare#('0(),'neg(y)) -> c_5() 'compare#('0(),'pos(y)) -> c_6() 'compare#('0(),'s(y)) -> c_7() 'compare#('neg(x),'0()) -> c_8() 'compare#('neg(x),'neg(y)) -> c_9('compare#(y,x)) 'compare#('neg(x),'pos(y)) -> c_10() 'compare#('pos(x),'0()) -> c_11() 'compare#('pos(x),'neg(y)) -> c_12() 'compare#('pos(x),'pos(y)) -> c_13('compare#(x,y)) 'compare#('s(x),'0()) -> c_14() 'compare#('s(x),'s(y)) -> c_15('compare#(x,y)) 'less#(x,y) -> c_16('cklt#('compare(x,y)),'compare#(x,y)) append#(l1,l2) -> c_17(append'1#(l1,l2)) append'1#(dd(x,xs),l2) -> c_18(append#(xs,l2)) append'1#(nil(),l2) -> c_19() flatten#(t) -> c_20(flatten'1#(t)) flatten'1#(leaf()) -> c_21() flatten'1#(node(l,t1,t2)) -> c_22(append#(l,append(flatten(t1),flatten(t2))) ,append#(flatten(t1),flatten(t2)) ,flatten#(t1) ,flatten#(t2)) flattensort#(t) -> c_23(insertionsort#(flatten(t)),flatten#(t)) insert#(x,l) -> c_24(insert'1#(l,x)) insert'1#(dd(y,ys),x) -> c_25(insert'2#('less(y,x),x,y,ys),'less#(y,x)) insert'1#(nil(),x) -> c_26() insert'2#('false(),x,y,ys) -> c_27() insert'2#('true(),x,y,ys) -> c_28(insert#(x,ys)) insertionsort#(l) -> c_29(insertionsort'1#(l)) insertionsort'1#(dd(x,xs)) -> c_30(insert#(x,insertionsort(xs)),insertionsort#(xs)) insertionsort'1#(nil()) -> c_31() Weak DPs and mark the set of starting terms. * Step 2: PredecessorEstimation WORST_CASE(?,O(n^3)) + Considered Problem: - Strict DPs: 'cklt#('EQ()) -> c_1() 'cklt#('GT()) -> c_2() 'cklt#('LT()) -> c_3() 'compare#('0(),'0()) -> c_4() 'compare#('0(),'neg(y)) -> c_5() 'compare#('0(),'pos(y)) -> c_6() 'compare#('0(),'s(y)) -> c_7() 'compare#('neg(x),'0()) -> c_8() 'compare#('neg(x),'neg(y)) -> c_9('compare#(y,x)) 'compare#('neg(x),'pos(y)) -> c_10() 'compare#('pos(x),'0()) -> c_11() 'compare#('pos(x),'neg(y)) -> c_12() 'compare#('pos(x),'pos(y)) -> c_13('compare#(x,y)) 'compare#('s(x),'0()) -> c_14() 'compare#('s(x),'s(y)) -> c_15('compare#(x,y)) 'less#(x,y) -> c_16('cklt#('compare(x,y)),'compare#(x,y)) append#(l1,l2) -> c_17(append'1#(l1,l2)) append'1#(dd(x,xs),l2) -> c_18(append#(xs,l2)) append'1#(nil(),l2) -> c_19() flatten#(t) -> c_20(flatten'1#(t)) flatten'1#(leaf()) -> c_21() flatten'1#(node(l,t1,t2)) -> c_22(append#(l,append(flatten(t1),flatten(t2))) ,append#(flatten(t1),flatten(t2)) ,flatten#(t1) ,flatten#(t2)) flattensort#(t) -> c_23(insertionsort#(flatten(t)),flatten#(t)) insert#(x,l) -> c_24(insert'1#(l,x)) insert'1#(dd(y,ys),x) -> c_25(insert'2#('less(y,x),x,y,ys),'less#(y,x)) insert'1#(nil(),x) -> c_26() insert'2#('false(),x,y,ys) -> c_27() insert'2#('true(),x,y,ys) -> c_28(insert#(x,ys)) insertionsort#(l) -> c_29(insertionsort'1#(l)) insertionsort'1#(dd(x,xs)) -> c_30(insert#(x,insertionsort(xs)),insertionsort#(xs)) insertionsort'1#(nil()) -> c_31() - Weak TRS: 'cklt('EQ()) -> 'false() 'cklt('GT()) -> 'false() 'cklt('LT()) -> 'true() 'compare('0(),'0()) -> 'EQ() 'compare('0(),'neg(y)) -> 'GT() 'compare('0(),'pos(y)) -> 'LT() 'compare('0(),'s(y)) -> 'LT() 'compare('neg(x),'0()) -> 'LT() 'compare('neg(x),'neg(y)) -> 'compare(y,x) 'compare('neg(x),'pos(y)) -> 'LT() 'compare('pos(x),'0()) -> 'GT() 'compare('pos(x),'neg(y)) -> 'GT() 'compare('pos(x),'pos(y)) -> 'compare(x,y) 'compare('s(x),'0()) -> 'GT() 'compare('s(x),'s(y)) -> 'compare(x,y) 'less(x,y) -> 'cklt('compare(x,y)) append(l1,l2) -> append'1(l1,l2) append'1(dd(x,xs),l2) -> dd(x,append(xs,l2)) append'1(nil(),l2) -> l2 flatten(t) -> flatten'1(t) flatten'1(leaf()) -> nil() flatten'1(node(l,t1,t2)) -> append(l,append(flatten(t1),flatten(t2))) flattensort(t) -> insertionsort(flatten(t)) insert(x,l) -> insert'1(l,x) insert'1(dd(y,ys),x) -> insert'2('less(y,x),x,y,ys) insert'1(nil(),x) -> dd(x,nil()) insert'2('false(),x,y,ys) -> dd(x,dd(y,ys)) insert'2('true(),x,y,ys) -> dd(y,insert(x,ys)) insertionsort(l) -> insertionsort'1(l) insertionsort'1(dd(x,xs)) -> insert(x,insertionsort(xs)) insertionsort'1(nil()) -> nil() - Signature: {'cklt/1,'compare/2,'less/2,append/2,append'1/2,flatten/1,flatten'1/1,flattensort/1,insert/2,insert'1/2 ,insert'2/4,insertionsort/1,insertionsort'1/1,'cklt#/1,'compare#/2,'less#/2,append#/2,append'1#/2,flatten#/1 ,flatten'1#/1,flattensort#/1,insert#/2,insert'1#/2,insert'2#/4,insertionsort#/1,insertionsort'1#/1} / {'0/0 ,'EQ/0,'GT/0,'LT/0,'false/0,'neg/1,'pos/1,'s/1,'true/0,dd/2,leaf/0,nil/0,node/3,c_1/0,c_2/0,c_3/0,c_4/0 ,c_5/0,c_6/0,c_7/0,c_8/0,c_9/1,c_10/0,c_11/0,c_12/0,c_13/1,c_14/0,c_15/1,c_16/2,c_17/1,c_18/1,c_19/0,c_20/1 ,c_21/0,c_22/4,c_23/2,c_24/1,c_25/2,c_26/0,c_27/0,c_28/1,c_29/1,c_30/2,c_31/0} - Obligation: innermost runtime complexity wrt. defined symbols {'cklt#,'compare#,'less#,append#,append'1#,flatten# ,flatten'1#,flattensort#,insert#,insert'1#,insert'2#,insertionsort#,insertionsort'1#} and constructors {'0 ,'EQ,'GT,'LT,'false,'neg,'pos,'s,'true,dd,leaf,nil,node} + Applied Processor: PredecessorEstimation {onSelection = all simple predecessor estimation selector} + Details: We estimate the number of application of {1,2,3,4,5,6,7,8,10,11,12,14,19,21,26,27,31} by application of Pre({1,2,3,4,5,6,7,8,10,11,12,14,19,21,26,27,31}) = {9,13,15,16,17,20,24,25,29}. Here rules are labelled as follows: 1: 'cklt#('EQ()) -> c_1() 2: 'cklt#('GT()) -> c_2() 3: 'cklt#('LT()) -> c_3() 4: 'compare#('0(),'0()) -> c_4() 5: 'compare#('0(),'neg(y)) -> c_5() 6: 'compare#('0(),'pos(y)) -> c_6() 7: 'compare#('0(),'s(y)) -> c_7() 8: 'compare#('neg(x),'0()) -> c_8() 9: 'compare#('neg(x),'neg(y)) -> c_9('compare#(y,x)) 10: 'compare#('neg(x),'pos(y)) -> c_10() 11: 'compare#('pos(x),'0()) -> c_11() 12: 'compare#('pos(x),'neg(y)) -> c_12() 13: 'compare#('pos(x),'pos(y)) -> c_13('compare#(x,y)) 14: 'compare#('s(x),'0()) -> c_14() 15: 'compare#('s(x),'s(y)) -> c_15('compare#(x,y)) 16: 'less#(x,y) -> c_16('cklt#('compare(x,y)),'compare#(x,y)) 17: append#(l1,l2) -> c_17(append'1#(l1,l2)) 18: append'1#(dd(x,xs),l2) -> c_18(append#(xs,l2)) 19: append'1#(nil(),l2) -> c_19() 20: flatten#(t) -> c_20(flatten'1#(t)) 21: flatten'1#(leaf()) -> c_21() 22: flatten'1#(node(l,t1,t2)) -> c_22(append#(l,append(flatten(t1),flatten(t2))) ,append#(flatten(t1),flatten(t2)) ,flatten#(t1) ,flatten#(t2)) 23: flattensort#(t) -> c_23(insertionsort#(flatten(t)),flatten#(t)) 24: insert#(x,l) -> c_24(insert'1#(l,x)) 25: insert'1#(dd(y,ys),x) -> c_25(insert'2#('less(y,x),x,y,ys),'less#(y,x)) 26: insert'1#(nil(),x) -> c_26() 27: insert'2#('false(),x,y,ys) -> c_27() 28: insert'2#('true(),x,y,ys) -> c_28(insert#(x,ys)) 29: insertionsort#(l) -> c_29(insertionsort'1#(l)) 30: insertionsort'1#(dd(x,xs)) -> c_30(insert#(x,insertionsort(xs)),insertionsort#(xs)) 31: insertionsort'1#(nil()) -> c_31() * Step 3: RemoveWeakSuffixes WORST_CASE(?,O(n^3)) + Considered Problem: - Strict DPs: 'compare#('neg(x),'neg(y)) -> c_9('compare#(y,x)) 'compare#('pos(x),'pos(y)) -> c_13('compare#(x,y)) 'compare#('s(x),'s(y)) -> c_15('compare#(x,y)) 'less#(x,y) -> c_16('cklt#('compare(x,y)),'compare#(x,y)) append#(l1,l2) -> c_17(append'1#(l1,l2)) append'1#(dd(x,xs),l2) -> c_18(append#(xs,l2)) flatten#(t) -> c_20(flatten'1#(t)) flatten'1#(node(l,t1,t2)) -> c_22(append#(l,append(flatten(t1),flatten(t2))) ,append#(flatten(t1),flatten(t2)) ,flatten#(t1) ,flatten#(t2)) flattensort#(t) -> c_23(insertionsort#(flatten(t)),flatten#(t)) insert#(x,l) -> c_24(insert'1#(l,x)) insert'1#(dd(y,ys),x) -> c_25(insert'2#('less(y,x),x,y,ys),'less#(y,x)) insert'2#('true(),x,y,ys) -> c_28(insert#(x,ys)) insertionsort#(l) -> c_29(insertionsort'1#(l)) insertionsort'1#(dd(x,xs)) -> c_30(insert#(x,insertionsort(xs)),insertionsort#(xs)) - Weak DPs: 'cklt#('EQ()) -> c_1() 'cklt#('GT()) -> c_2() 'cklt#('LT()) -> c_3() 'compare#('0(),'0()) -> c_4() 'compare#('0(),'neg(y)) -> c_5() 'compare#('0(),'pos(y)) -> c_6() 'compare#('0(),'s(y)) -> c_7() 'compare#('neg(x),'0()) -> c_8() 'compare#('neg(x),'pos(y)) -> c_10() 'compare#('pos(x),'0()) -> c_11() 'compare#('pos(x),'neg(y)) -> c_12() 'compare#('s(x),'0()) -> c_14() append'1#(nil(),l2) -> c_19() flatten'1#(leaf()) -> c_21() insert'1#(nil(),x) -> c_26() insert'2#('false(),x,y,ys) -> c_27() insertionsort'1#(nil()) -> c_31() - Weak TRS: 'cklt('EQ()) -> 'false() 'cklt('GT()) -> 'false() 'cklt('LT()) -> 'true() 'compare('0(),'0()) -> 'EQ() 'compare('0(),'neg(y)) -> 'GT() 'compare('0(),'pos(y)) -> 'LT() 'compare('0(),'s(y)) -> 'LT() 'compare('neg(x),'0()) -> 'LT() 'compare('neg(x),'neg(y)) -> 'compare(y,x) 'compare('neg(x),'pos(y)) -> 'LT() 'compare('pos(x),'0()) -> 'GT() 'compare('pos(x),'neg(y)) -> 'GT() 'compare('pos(x),'pos(y)) -> 'compare(x,y) 'compare('s(x),'0()) -> 'GT() 'compare('s(x),'s(y)) -> 'compare(x,y) 'less(x,y) -> 'cklt('compare(x,y)) append(l1,l2) -> append'1(l1,l2) append'1(dd(x,xs),l2) -> dd(x,append(xs,l2)) append'1(nil(),l2) -> l2 flatten(t) -> flatten'1(t) flatten'1(leaf()) -> nil() flatten'1(node(l,t1,t2)) -> append(l,append(flatten(t1),flatten(t2))) flattensort(t) -> insertionsort(flatten(t)) insert(x,l) -> insert'1(l,x) insert'1(dd(y,ys),x) -> insert'2('less(y,x),x,y,ys) insert'1(nil(),x) -> dd(x,nil()) insert'2('false(),x,y,ys) -> dd(x,dd(y,ys)) insert'2('true(),x,y,ys) -> dd(y,insert(x,ys)) insertionsort(l) -> insertionsort'1(l) insertionsort'1(dd(x,xs)) -> insert(x,insertionsort(xs)) insertionsort'1(nil()) -> nil() - Signature: {'cklt/1,'compare/2,'less/2,append/2,append'1/2,flatten/1,flatten'1/1,flattensort/1,insert/2,insert'1/2 ,insert'2/4,insertionsort/1,insertionsort'1/1,'cklt#/1,'compare#/2,'less#/2,append#/2,append'1#/2,flatten#/1 ,flatten'1#/1,flattensort#/1,insert#/2,insert'1#/2,insert'2#/4,insertionsort#/1,insertionsort'1#/1} / {'0/0 ,'EQ/0,'GT/0,'LT/0,'false/0,'neg/1,'pos/1,'s/1,'true/0,dd/2,leaf/0,nil/0,node/3,c_1/0,c_2/0,c_3/0,c_4/0 ,c_5/0,c_6/0,c_7/0,c_8/0,c_9/1,c_10/0,c_11/0,c_12/0,c_13/1,c_14/0,c_15/1,c_16/2,c_17/1,c_18/1,c_19/0,c_20/1 ,c_21/0,c_22/4,c_23/2,c_24/1,c_25/2,c_26/0,c_27/0,c_28/1,c_29/1,c_30/2,c_31/0} - Obligation: innermost runtime complexity wrt. defined symbols {'cklt#,'compare#,'less#,append#,append'1#,flatten# ,flatten'1#,flattensort#,insert#,insert'1#,insert'2#,insertionsort#,insertionsort'1#} and constructors {'0 ,'EQ,'GT,'LT,'false,'neg,'pos,'s,'true,dd,leaf,nil,node} + Applied Processor: RemoveWeakSuffixes + Details: Consider the dependency graph 1:S:'compare#('neg(x),'neg(y)) -> c_9('compare#(y,x)) -->_1 'compare#('s(x),'s(y)) -> c_15('compare#(x,y)):3 -->_1 'compare#('pos(x),'pos(y)) -> c_13('compare#(x,y)):2 -->_1 'compare#('s(x),'0()) -> c_14():26 -->_1 'compare#('pos(x),'neg(y)) -> c_12():25 -->_1 'compare#('pos(x),'0()) -> c_11():24 -->_1 'compare#('neg(x),'pos(y)) -> c_10():23 -->_1 'compare#('neg(x),'0()) -> c_8():22 -->_1 'compare#('0(),'s(y)) -> c_7():21 -->_1 'compare#('0(),'pos(y)) -> c_6():20 -->_1 'compare#('0(),'neg(y)) -> c_5():19 -->_1 'compare#('0(),'0()) -> c_4():18 -->_1 'compare#('neg(x),'neg(y)) -> c_9('compare#(y,x)):1 2:S:'compare#('pos(x),'pos(y)) -> c_13('compare#(x,y)) -->_1 'compare#('s(x),'s(y)) -> c_15('compare#(x,y)):3 -->_1 'compare#('s(x),'0()) -> c_14():26 -->_1 'compare#('pos(x),'neg(y)) -> c_12():25 -->_1 'compare#('pos(x),'0()) -> c_11():24 -->_1 'compare#('neg(x),'pos(y)) -> c_10():23 -->_1 'compare#('neg(x),'0()) -> c_8():22 -->_1 'compare#('0(),'s(y)) -> c_7():21 -->_1 'compare#('0(),'pos(y)) -> c_6():20 -->_1 'compare#('0(),'neg(y)) -> c_5():19 -->_1 'compare#('0(),'0()) -> c_4():18 -->_1 'compare#('pos(x),'pos(y)) -> c_13('compare#(x,y)):2 -->_1 'compare#('neg(x),'neg(y)) -> c_9('compare#(y,x)):1 3:S:'compare#('s(x),'s(y)) -> c_15('compare#(x,y)) -->_1 'compare#('s(x),'0()) -> c_14():26 -->_1 'compare#('pos(x),'neg(y)) -> c_12():25 -->_1 'compare#('pos(x),'0()) -> c_11():24 -->_1 'compare#('neg(x),'pos(y)) -> c_10():23 -->_1 'compare#('neg(x),'0()) -> c_8():22 -->_1 'compare#('0(),'s(y)) -> c_7():21 -->_1 'compare#('0(),'pos(y)) -> c_6():20 -->_1 'compare#('0(),'neg(y)) -> c_5():19 -->_1 'compare#('0(),'0()) -> c_4():18 -->_1 'compare#('s(x),'s(y)) -> c_15('compare#(x,y)):3 -->_1 'compare#('pos(x),'pos(y)) -> c_13('compare#(x,y)):2 -->_1 'compare#('neg(x),'neg(y)) -> c_9('compare#(y,x)):1 4:S:'less#(x,y) -> c_16('cklt#('compare(x,y)),'compare#(x,y)) -->_2 'compare#('s(x),'0()) -> c_14():26 -->_2 'compare#('pos(x),'neg(y)) -> c_12():25 -->_2 'compare#('pos(x),'0()) -> c_11():24 -->_2 'compare#('neg(x),'pos(y)) -> c_10():23 -->_2 'compare#('neg(x),'0()) -> c_8():22 -->_2 'compare#('0(),'s(y)) -> c_7():21 -->_2 'compare#('0(),'pos(y)) -> c_6():20 -->_2 'compare#('0(),'neg(y)) -> c_5():19 -->_2 'compare#('0(),'0()) -> c_4():18 -->_1 'cklt#('LT()) -> c_3():17 -->_1 'cklt#('GT()) -> c_2():16 -->_1 'cklt#('EQ()) -> c_1():15 -->_2 'compare#('s(x),'s(y)) -> c_15('compare#(x,y)):3 -->_2 'compare#('pos(x),'pos(y)) -> c_13('compare#(x,y)):2 -->_2 'compare#('neg(x),'neg(y)) -> c_9('compare#(y,x)):1 5:S:append#(l1,l2) -> c_17(append'1#(l1,l2)) -->_1 append'1#(dd(x,xs),l2) -> c_18(append#(xs,l2)):6 -->_1 append'1#(nil(),l2) -> c_19():27 6:S:append'1#(dd(x,xs),l2) -> c_18(append#(xs,l2)) -->_1 append#(l1,l2) -> c_17(append'1#(l1,l2)):5 7:S:flatten#(t) -> c_20(flatten'1#(t)) -->_1 flatten'1#(node(l,t1,t2)) -> c_22(append#(l,append(flatten(t1),flatten(t2))) ,append#(flatten(t1),flatten(t2)) ,flatten#(t1) ,flatten#(t2)):8 -->_1 flatten'1#(leaf()) -> c_21():28 8:S:flatten'1#(node(l,t1,t2)) -> c_22(append#(l,append(flatten(t1),flatten(t2))) ,append#(flatten(t1),flatten(t2)) ,flatten#(t1) ,flatten#(t2)) -->_4 flatten#(t) -> c_20(flatten'1#(t)):7 -->_3 flatten#(t) -> c_20(flatten'1#(t)):7 -->_2 append#(l1,l2) -> c_17(append'1#(l1,l2)):5 -->_1 append#(l1,l2) -> c_17(append'1#(l1,l2)):5 9:S:flattensort#(t) -> c_23(insertionsort#(flatten(t)),flatten#(t)) -->_1 insertionsort#(l) -> c_29(insertionsort'1#(l)):13 -->_2 flatten#(t) -> c_20(flatten'1#(t)):7 10:S:insert#(x,l) -> c_24(insert'1#(l,x)) -->_1 insert'1#(dd(y,ys),x) -> c_25(insert'2#('less(y,x),x,y,ys),'less#(y,x)):11 -->_1 insert'1#(nil(),x) -> c_26():29 11:S:insert'1#(dd(y,ys),x) -> c_25(insert'2#('less(y,x),x,y,ys),'less#(y,x)) -->_1 insert'2#('true(),x,y,ys) -> c_28(insert#(x,ys)):12 -->_1 insert'2#('false(),x,y,ys) -> c_27():30 -->_2 'less#(x,y) -> c_16('cklt#('compare(x,y)),'compare#(x,y)):4 12:S:insert'2#('true(),x,y,ys) -> c_28(insert#(x,ys)) -->_1 insert#(x,l) -> c_24(insert'1#(l,x)):10 13:S:insertionsort#(l) -> c_29(insertionsort'1#(l)) -->_1 insertionsort'1#(dd(x,xs)) -> c_30(insert#(x,insertionsort(xs)),insertionsort#(xs)):14 -->_1 insertionsort'1#(nil()) -> c_31():31 14:S:insertionsort'1#(dd(x,xs)) -> c_30(insert#(x,insertionsort(xs)),insertionsort#(xs)) -->_2 insertionsort#(l) -> c_29(insertionsort'1#(l)):13 -->_1 insert#(x,l) -> c_24(insert'1#(l,x)):10 15:W:'cklt#('EQ()) -> c_1() 16:W:'cklt#('GT()) -> c_2() 17:W:'cklt#('LT()) -> c_3() 18:W:'compare#('0(),'0()) -> c_4() 19:W:'compare#('0(),'neg(y)) -> c_5() 20:W:'compare#('0(),'pos(y)) -> c_6() 21:W:'compare#('0(),'s(y)) -> c_7() 22:W:'compare#('neg(x),'0()) -> c_8() 23:W:'compare#('neg(x),'pos(y)) -> c_10() 24:W:'compare#('pos(x),'0()) -> c_11() 25:W:'compare#('pos(x),'neg(y)) -> c_12() 26:W:'compare#('s(x),'0()) -> c_14() 27:W:append'1#(nil(),l2) -> c_19() 28:W:flatten'1#(leaf()) -> c_21() 29:W:insert'1#(nil(),x) -> c_26() 30:W:insert'2#('false(),x,y,ys) -> c_27() 31:W:insertionsort'1#(nil()) -> c_31() The following weak DPs constitute a sub-graph of the DG that is closed under successors. The DPs are removed. 31: insertionsort'1#(nil()) -> c_31() 29: insert'1#(nil(),x) -> c_26() 30: insert'2#('false(),x,y,ys) -> c_27() 28: flatten'1#(leaf()) -> c_21() 27: append'1#(nil(),l2) -> c_19() 15: 'cklt#('EQ()) -> c_1() 16: 'cklt#('GT()) -> c_2() 17: 'cklt#('LT()) -> c_3() 18: 'compare#('0(),'0()) -> c_4() 19: 'compare#('0(),'neg(y)) -> c_5() 20: 'compare#('0(),'pos(y)) -> c_6() 21: 'compare#('0(),'s(y)) -> c_7() 22: 'compare#('neg(x),'0()) -> c_8() 23: 'compare#('neg(x),'pos(y)) -> c_10() 24: 'compare#('pos(x),'0()) -> c_11() 25: 'compare#('pos(x),'neg(y)) -> c_12() 26: 'compare#('s(x),'0()) -> c_14() * Step 4: SimplifyRHS WORST_CASE(?,O(n^3)) + Considered Problem: - Strict DPs: 'compare#('neg(x),'neg(y)) -> c_9('compare#(y,x)) 'compare#('pos(x),'pos(y)) -> c_13('compare#(x,y)) 'compare#('s(x),'s(y)) -> c_15('compare#(x,y)) 'less#(x,y) -> c_16('cklt#('compare(x,y)),'compare#(x,y)) append#(l1,l2) -> c_17(append'1#(l1,l2)) append'1#(dd(x,xs),l2) -> c_18(append#(xs,l2)) flatten#(t) -> c_20(flatten'1#(t)) flatten'1#(node(l,t1,t2)) -> c_22(append#(l,append(flatten(t1),flatten(t2))) ,append#(flatten(t1),flatten(t2)) ,flatten#(t1) ,flatten#(t2)) flattensort#(t) -> c_23(insertionsort#(flatten(t)),flatten#(t)) insert#(x,l) -> c_24(insert'1#(l,x)) insert'1#(dd(y,ys),x) -> c_25(insert'2#('less(y,x),x,y,ys),'less#(y,x)) insert'2#('true(),x,y,ys) -> c_28(insert#(x,ys)) insertionsort#(l) -> c_29(insertionsort'1#(l)) insertionsort'1#(dd(x,xs)) -> c_30(insert#(x,insertionsort(xs)),insertionsort#(xs)) - Weak TRS: 'cklt('EQ()) -> 'false() 'cklt('GT()) -> 'false() 'cklt('LT()) -> 'true() 'compare('0(),'0()) -> 'EQ() 'compare('0(),'neg(y)) -> 'GT() 'compare('0(),'pos(y)) -> 'LT() 'compare('0(),'s(y)) -> 'LT() 'compare('neg(x),'0()) -> 'LT() 'compare('neg(x),'neg(y)) -> 'compare(y,x) 'compare('neg(x),'pos(y)) -> 'LT() 'compare('pos(x),'0()) -> 'GT() 'compare('pos(x),'neg(y)) -> 'GT() 'compare('pos(x),'pos(y)) -> 'compare(x,y) 'compare('s(x),'0()) -> 'GT() 'compare('s(x),'s(y)) -> 'compare(x,y) 'less(x,y) -> 'cklt('compare(x,y)) append(l1,l2) -> append'1(l1,l2) append'1(dd(x,xs),l2) -> dd(x,append(xs,l2)) append'1(nil(),l2) -> l2 flatten(t) -> flatten'1(t) flatten'1(leaf()) -> nil() flatten'1(node(l,t1,t2)) -> append(l,append(flatten(t1),flatten(t2))) flattensort(t) -> insertionsort(flatten(t)) insert(x,l) -> insert'1(l,x) insert'1(dd(y,ys),x) -> insert'2('less(y,x),x,y,ys) insert'1(nil(),x) -> dd(x,nil()) insert'2('false(),x,y,ys) -> dd(x,dd(y,ys)) insert'2('true(),x,y,ys) -> dd(y,insert(x,ys)) insertionsort(l) -> insertionsort'1(l) insertionsort'1(dd(x,xs)) -> insert(x,insertionsort(xs)) insertionsort'1(nil()) -> nil() - Signature: {'cklt/1,'compare/2,'less/2,append/2,append'1/2,flatten/1,flatten'1/1,flattensort/1,insert/2,insert'1/2 ,insert'2/4,insertionsort/1,insertionsort'1/1,'cklt#/1,'compare#/2,'less#/2,append#/2,append'1#/2,flatten#/1 ,flatten'1#/1,flattensort#/1,insert#/2,insert'1#/2,insert'2#/4,insertionsort#/1,insertionsort'1#/1} / {'0/0 ,'EQ/0,'GT/0,'LT/0,'false/0,'neg/1,'pos/1,'s/1,'true/0,dd/2,leaf/0,nil/0,node/3,c_1/0,c_2/0,c_3/0,c_4/0 ,c_5/0,c_6/0,c_7/0,c_8/0,c_9/1,c_10/0,c_11/0,c_12/0,c_13/1,c_14/0,c_15/1,c_16/2,c_17/1,c_18/1,c_19/0,c_20/1 ,c_21/0,c_22/4,c_23/2,c_24/1,c_25/2,c_26/0,c_27/0,c_28/1,c_29/1,c_30/2,c_31/0} - Obligation: innermost runtime complexity wrt. defined symbols {'cklt#,'compare#,'less#,append#,append'1#,flatten# ,flatten'1#,flattensort#,insert#,insert'1#,insert'2#,insertionsort#,insertionsort'1#} and constructors {'0 ,'EQ,'GT,'LT,'false,'neg,'pos,'s,'true,dd,leaf,nil,node} + Applied Processor: SimplifyRHS + Details: Consider the dependency graph 1:S:'compare#('neg(x),'neg(y)) -> c_9('compare#(y,x)) -->_1 'compare#('s(x),'s(y)) -> c_15('compare#(x,y)):3 -->_1 'compare#('pos(x),'pos(y)) -> c_13('compare#(x,y)):2 -->_1 'compare#('neg(x),'neg(y)) -> c_9('compare#(y,x)):1 2:S:'compare#('pos(x),'pos(y)) -> c_13('compare#(x,y)) -->_1 'compare#('s(x),'s(y)) -> c_15('compare#(x,y)):3 -->_1 'compare#('pos(x),'pos(y)) -> c_13('compare#(x,y)):2 -->_1 'compare#('neg(x),'neg(y)) -> c_9('compare#(y,x)):1 3:S:'compare#('s(x),'s(y)) -> c_15('compare#(x,y)) -->_1 'compare#('s(x),'s(y)) -> c_15('compare#(x,y)):3 -->_1 'compare#('pos(x),'pos(y)) -> c_13('compare#(x,y)):2 -->_1 'compare#('neg(x),'neg(y)) -> c_9('compare#(y,x)):1 4:S:'less#(x,y) -> c_16('cklt#('compare(x,y)),'compare#(x,y)) -->_2 'compare#('s(x),'s(y)) -> c_15('compare#(x,y)):3 -->_2 'compare#('pos(x),'pos(y)) -> c_13('compare#(x,y)):2 -->_2 'compare#('neg(x),'neg(y)) -> c_9('compare#(y,x)):1 5:S:append#(l1,l2) -> c_17(append'1#(l1,l2)) -->_1 append'1#(dd(x,xs),l2) -> c_18(append#(xs,l2)):6 6:S:append'1#(dd(x,xs),l2) -> c_18(append#(xs,l2)) -->_1 append#(l1,l2) -> c_17(append'1#(l1,l2)):5 7:S:flatten#(t) -> c_20(flatten'1#(t)) -->_1 flatten'1#(node(l,t1,t2)) -> c_22(append#(l,append(flatten(t1),flatten(t2))) ,append#(flatten(t1),flatten(t2)) ,flatten#(t1) ,flatten#(t2)):8 8:S:flatten'1#(node(l,t1,t2)) -> c_22(append#(l,append(flatten(t1),flatten(t2))) ,append#(flatten(t1),flatten(t2)) ,flatten#(t1) ,flatten#(t2)) -->_4 flatten#(t) -> c_20(flatten'1#(t)):7 -->_3 flatten#(t) -> c_20(flatten'1#(t)):7 -->_2 append#(l1,l2) -> c_17(append'1#(l1,l2)):5 -->_1 append#(l1,l2) -> c_17(append'1#(l1,l2)):5 9:S:flattensort#(t) -> c_23(insertionsort#(flatten(t)),flatten#(t)) -->_1 insertionsort#(l) -> c_29(insertionsort'1#(l)):13 -->_2 flatten#(t) -> c_20(flatten'1#(t)):7 10:S:insert#(x,l) -> c_24(insert'1#(l,x)) -->_1 insert'1#(dd(y,ys),x) -> c_25(insert'2#('less(y,x),x,y,ys),'less#(y,x)):11 11:S:insert'1#(dd(y,ys),x) -> c_25(insert'2#('less(y,x),x,y,ys),'less#(y,x)) -->_1 insert'2#('true(),x,y,ys) -> c_28(insert#(x,ys)):12 -->_2 'less#(x,y) -> c_16('cklt#('compare(x,y)),'compare#(x,y)):4 12:S:insert'2#('true(),x,y,ys) -> c_28(insert#(x,ys)) -->_1 insert#(x,l) -> c_24(insert'1#(l,x)):10 13:S:insertionsort#(l) -> c_29(insertionsort'1#(l)) -->_1 insertionsort'1#(dd(x,xs)) -> c_30(insert#(x,insertionsort(xs)),insertionsort#(xs)):14 14:S:insertionsort'1#(dd(x,xs)) -> c_30(insert#(x,insertionsort(xs)),insertionsort#(xs)) -->_2 insertionsort#(l) -> c_29(insertionsort'1#(l)):13 -->_1 insert#(x,l) -> c_24(insert'1#(l,x)):10 Due to missing edges in the depndency graph, the right-hand sides of following rules could be simplified: 'less#(x,y) -> c_16('compare#(x,y)) * Step 5: UsableRules WORST_CASE(?,O(n^3)) + Considered Problem: - Strict DPs: 'compare#('neg(x),'neg(y)) -> c_9('compare#(y,x)) 'compare#('pos(x),'pos(y)) -> c_13('compare#(x,y)) 'compare#('s(x),'s(y)) -> c_15('compare#(x,y)) 'less#(x,y) -> c_16('compare#(x,y)) append#(l1,l2) -> c_17(append'1#(l1,l2)) append'1#(dd(x,xs),l2) -> c_18(append#(xs,l2)) flatten#(t) -> c_20(flatten'1#(t)) flatten'1#(node(l,t1,t2)) -> c_22(append#(l,append(flatten(t1),flatten(t2))) ,append#(flatten(t1),flatten(t2)) ,flatten#(t1) ,flatten#(t2)) flattensort#(t) -> c_23(insertionsort#(flatten(t)),flatten#(t)) insert#(x,l) -> c_24(insert'1#(l,x)) insert'1#(dd(y,ys),x) -> c_25(insert'2#('less(y,x),x,y,ys),'less#(y,x)) insert'2#('true(),x,y,ys) -> c_28(insert#(x,ys)) insertionsort#(l) -> c_29(insertionsort'1#(l)) insertionsort'1#(dd(x,xs)) -> c_30(insert#(x,insertionsort(xs)),insertionsort#(xs)) - Weak TRS: 'cklt('EQ()) -> 'false() 'cklt('GT()) -> 'false() 'cklt('LT()) -> 'true() 'compare('0(),'0()) -> 'EQ() 'compare('0(),'neg(y)) -> 'GT() 'compare('0(),'pos(y)) -> 'LT() 'compare('0(),'s(y)) -> 'LT() 'compare('neg(x),'0()) -> 'LT() 'compare('neg(x),'neg(y)) -> 'compare(y,x) 'compare('neg(x),'pos(y)) -> 'LT() 'compare('pos(x),'0()) -> 'GT() 'compare('pos(x),'neg(y)) -> 'GT() 'compare('pos(x),'pos(y)) -> 'compare(x,y) 'compare('s(x),'0()) -> 'GT() 'compare('s(x),'s(y)) -> 'compare(x,y) 'less(x,y) -> 'cklt('compare(x,y)) append(l1,l2) -> append'1(l1,l2) append'1(dd(x,xs),l2) -> dd(x,append(xs,l2)) append'1(nil(),l2) -> l2 flatten(t) -> flatten'1(t) flatten'1(leaf()) -> nil() flatten'1(node(l,t1,t2)) -> append(l,append(flatten(t1),flatten(t2))) flattensort(t) -> insertionsort(flatten(t)) insert(x,l) -> insert'1(l,x) insert'1(dd(y,ys),x) -> insert'2('less(y,x),x,y,ys) insert'1(nil(),x) -> dd(x,nil()) insert'2('false(),x,y,ys) -> dd(x,dd(y,ys)) insert'2('true(),x,y,ys) -> dd(y,insert(x,ys)) insertionsort(l) -> insertionsort'1(l) insertionsort'1(dd(x,xs)) -> insert(x,insertionsort(xs)) insertionsort'1(nil()) -> nil() - Signature: {'cklt/1,'compare/2,'less/2,append/2,append'1/2,flatten/1,flatten'1/1,flattensort/1,insert/2,insert'1/2 ,insert'2/4,insertionsort/1,insertionsort'1/1,'cklt#/1,'compare#/2,'less#/2,append#/2,append'1#/2,flatten#/1 ,flatten'1#/1,flattensort#/1,insert#/2,insert'1#/2,insert'2#/4,insertionsort#/1,insertionsort'1#/1} / {'0/0 ,'EQ/0,'GT/0,'LT/0,'false/0,'neg/1,'pos/1,'s/1,'true/0,dd/2,leaf/0,nil/0,node/3,c_1/0,c_2/0,c_3/0,c_4/0 ,c_5/0,c_6/0,c_7/0,c_8/0,c_9/1,c_10/0,c_11/0,c_12/0,c_13/1,c_14/0,c_15/1,c_16/1,c_17/1,c_18/1,c_19/0,c_20/1 ,c_21/0,c_22/4,c_23/2,c_24/1,c_25/2,c_26/0,c_27/0,c_28/1,c_29/1,c_30/2,c_31/0} - Obligation: innermost runtime complexity wrt. defined symbols {'cklt#,'compare#,'less#,append#,append'1#,flatten# ,flatten'1#,flattensort#,insert#,insert'1#,insert'2#,insertionsort#,insertionsort'1#} and constructors {'0 ,'EQ,'GT,'LT,'false,'neg,'pos,'s,'true,dd,leaf,nil,node} + Applied Processor: UsableRules + Details: We replace rewrite rules by usable rules: 'cklt('EQ()) -> 'false() 'cklt('GT()) -> 'false() 'cklt('LT()) -> 'true() 'compare('0(),'0()) -> 'EQ() 'compare('0(),'neg(y)) -> 'GT() 'compare('0(),'pos(y)) -> 'LT() 'compare('0(),'s(y)) -> 'LT() 'compare('neg(x),'0()) -> 'LT() 'compare('neg(x),'neg(y)) -> 'compare(y,x) 'compare('neg(x),'pos(y)) -> 'LT() 'compare('pos(x),'0()) -> 'GT() 'compare('pos(x),'neg(y)) -> 'GT() 'compare('pos(x),'pos(y)) -> 'compare(x,y) 'compare('s(x),'0()) -> 'GT() 'compare('s(x),'s(y)) -> 'compare(x,y) 'less(x,y) -> 'cklt('compare(x,y)) append(l1,l2) -> append'1(l1,l2) append'1(dd(x,xs),l2) -> dd(x,append(xs,l2)) append'1(nil(),l2) -> l2 flatten(t) -> flatten'1(t) flatten'1(leaf()) -> nil() flatten'1(node(l,t1,t2)) -> append(l,append(flatten(t1),flatten(t2))) insert(x,l) -> insert'1(l,x) insert'1(dd(y,ys),x) -> insert'2('less(y,x),x,y,ys) insert'1(nil(),x) -> dd(x,nil()) insert'2('false(),x,y,ys) -> dd(x,dd(y,ys)) insert'2('true(),x,y,ys) -> dd(y,insert(x,ys)) insertionsort(l) -> insertionsort'1(l) insertionsort'1(dd(x,xs)) -> insert(x,insertionsort(xs)) insertionsort'1(nil()) -> nil() 'compare#('neg(x),'neg(y)) -> c_9('compare#(y,x)) 'compare#('pos(x),'pos(y)) -> c_13('compare#(x,y)) 'compare#('s(x),'s(y)) -> c_15('compare#(x,y)) 'less#(x,y) -> c_16('compare#(x,y)) append#(l1,l2) -> c_17(append'1#(l1,l2)) append'1#(dd(x,xs),l2) -> c_18(append#(xs,l2)) flatten#(t) -> c_20(flatten'1#(t)) flatten'1#(node(l,t1,t2)) -> c_22(append#(l,append(flatten(t1),flatten(t2))) ,append#(flatten(t1),flatten(t2)) ,flatten#(t1) ,flatten#(t2)) flattensort#(t) -> c_23(insertionsort#(flatten(t)),flatten#(t)) insert#(x,l) -> c_24(insert'1#(l,x)) insert'1#(dd(y,ys),x) -> c_25(insert'2#('less(y,x),x,y,ys),'less#(y,x)) insert'2#('true(),x,y,ys) -> c_28(insert#(x,ys)) insertionsort#(l) -> c_29(insertionsort'1#(l)) insertionsort'1#(dd(x,xs)) -> c_30(insert#(x,insertionsort(xs)),insertionsort#(xs)) * Step 6: DecomposeDG WORST_CASE(?,O(n^3)) + Considered Problem: - Strict DPs: 'compare#('neg(x),'neg(y)) -> c_9('compare#(y,x)) 'compare#('pos(x),'pos(y)) -> c_13('compare#(x,y)) 'compare#('s(x),'s(y)) -> c_15('compare#(x,y)) 'less#(x,y) -> c_16('compare#(x,y)) append#(l1,l2) -> c_17(append'1#(l1,l2)) append'1#(dd(x,xs),l2) -> c_18(append#(xs,l2)) flatten#(t) -> c_20(flatten'1#(t)) flatten'1#(node(l,t1,t2)) -> c_22(append#(l,append(flatten(t1),flatten(t2))) ,append#(flatten(t1),flatten(t2)) ,flatten#(t1) ,flatten#(t2)) flattensort#(t) -> c_23(insertionsort#(flatten(t)),flatten#(t)) insert#(x,l) -> c_24(insert'1#(l,x)) insert'1#(dd(y,ys),x) -> c_25(insert'2#('less(y,x),x,y,ys),'less#(y,x)) insert'2#('true(),x,y,ys) -> c_28(insert#(x,ys)) insertionsort#(l) -> c_29(insertionsort'1#(l)) insertionsort'1#(dd(x,xs)) -> c_30(insert#(x,insertionsort(xs)),insertionsort#(xs)) - Weak TRS: 'cklt('EQ()) -> 'false() 'cklt('GT()) -> 'false() 'cklt('LT()) -> 'true() 'compare('0(),'0()) -> 'EQ() 'compare('0(),'neg(y)) -> 'GT() 'compare('0(),'pos(y)) -> 'LT() 'compare('0(),'s(y)) -> 'LT() 'compare('neg(x),'0()) -> 'LT() 'compare('neg(x),'neg(y)) -> 'compare(y,x) 'compare('neg(x),'pos(y)) -> 'LT() 'compare('pos(x),'0()) -> 'GT() 'compare('pos(x),'neg(y)) -> 'GT() 'compare('pos(x),'pos(y)) -> 'compare(x,y) 'compare('s(x),'0()) -> 'GT() 'compare('s(x),'s(y)) -> 'compare(x,y) 'less(x,y) -> 'cklt('compare(x,y)) append(l1,l2) -> append'1(l1,l2) append'1(dd(x,xs),l2) -> dd(x,append(xs,l2)) append'1(nil(),l2) -> l2 flatten(t) -> flatten'1(t) flatten'1(leaf()) -> nil() flatten'1(node(l,t1,t2)) -> append(l,append(flatten(t1),flatten(t2))) insert(x,l) -> insert'1(l,x) insert'1(dd(y,ys),x) -> insert'2('less(y,x),x,y,ys) insert'1(nil(),x) -> dd(x,nil()) insert'2('false(),x,y,ys) -> dd(x,dd(y,ys)) insert'2('true(),x,y,ys) -> dd(y,insert(x,ys)) insertionsort(l) -> insertionsort'1(l) insertionsort'1(dd(x,xs)) -> insert(x,insertionsort(xs)) insertionsort'1(nil()) -> nil() - Signature: {'cklt/1,'compare/2,'less/2,append/2,append'1/2,flatten/1,flatten'1/1,flattensort/1,insert/2,insert'1/2 ,insert'2/4,insertionsort/1,insertionsort'1/1,'cklt#/1,'compare#/2,'less#/2,append#/2,append'1#/2,flatten#/1 ,flatten'1#/1,flattensort#/1,insert#/2,insert'1#/2,insert'2#/4,insertionsort#/1,insertionsort'1#/1} / {'0/0 ,'EQ/0,'GT/0,'LT/0,'false/0,'neg/1,'pos/1,'s/1,'true/0,dd/2,leaf/0,nil/0,node/3,c_1/0,c_2/0,c_3/0,c_4/0 ,c_5/0,c_6/0,c_7/0,c_8/0,c_9/1,c_10/0,c_11/0,c_12/0,c_13/1,c_14/0,c_15/1,c_16/1,c_17/1,c_18/1,c_19/0,c_20/1 ,c_21/0,c_22/4,c_23/2,c_24/1,c_25/2,c_26/0,c_27/0,c_28/1,c_29/1,c_30/2,c_31/0} - Obligation: innermost runtime complexity wrt. defined symbols {'cklt#,'compare#,'less#,append#,append'1#,flatten# ,flatten'1#,flattensort#,insert#,insert'1#,insert'2#,insertionsort#,insertionsort'1#} and constructors {'0 ,'EQ,'GT,'LT,'false,'neg,'pos,'s,'true,dd,leaf,nil,node} + Applied Processor: DecomposeDG {onSelection = all below first cut in WDG, onUpper = Nothing, onLower = Nothing} + Details: We decompose the input problem according to the dependency graph into the upper component flatten#(t) -> c_20(flatten'1#(t)) flatten'1#(node(l,t1,t2)) -> c_22(append#(l,append(flatten(t1),flatten(t2))) ,append#(flatten(t1),flatten(t2)) ,flatten#(t1) ,flatten#(t2)) flattensort#(t) -> c_23(insertionsort#(flatten(t)),flatten#(t)) insertionsort#(l) -> c_29(insertionsort'1#(l)) insertionsort'1#(dd(x,xs)) -> c_30(insert#(x,insertionsort(xs)),insertionsort#(xs)) and a lower component 'compare#('neg(x),'neg(y)) -> c_9('compare#(y,x)) 'compare#('pos(x),'pos(y)) -> c_13('compare#(x,y)) 'compare#('s(x),'s(y)) -> c_15('compare#(x,y)) 'less#(x,y) -> c_16('compare#(x,y)) append#(l1,l2) -> c_17(append'1#(l1,l2)) append'1#(dd(x,xs),l2) -> c_18(append#(xs,l2)) insert#(x,l) -> c_24(insert'1#(l,x)) insert'1#(dd(y,ys),x) -> c_25(insert'2#('less(y,x),x,y,ys),'less#(y,x)) insert'2#('true(),x,y,ys) -> c_28(insert#(x,ys)) Further, following extension rules are added to the lower component. flatten#(t) -> flatten'1#(t) flatten'1#(node(l,t1,t2)) -> append#(l,append(flatten(t1),flatten(t2))) flatten'1#(node(l,t1,t2)) -> append#(flatten(t1),flatten(t2)) flatten'1#(node(l,t1,t2)) -> flatten#(t1) flatten'1#(node(l,t1,t2)) -> flatten#(t2) flattensort#(t) -> flatten#(t) flattensort#(t) -> insertionsort#(flatten(t)) insertionsort#(l) -> insertionsort'1#(l) insertionsort'1#(dd(x,xs)) -> insert#(x,insertionsort(xs)) insertionsort'1#(dd(x,xs)) -> insertionsort#(xs) ** Step 6.a:1: SimplifyRHS WORST_CASE(?,O(n^1)) + Considered Problem: - Strict DPs: flatten#(t) -> c_20(flatten'1#(t)) flatten'1#(node(l,t1,t2)) -> c_22(append#(l,append(flatten(t1),flatten(t2))) ,append#(flatten(t1),flatten(t2)) ,flatten#(t1) ,flatten#(t2)) flattensort#(t) -> c_23(insertionsort#(flatten(t)),flatten#(t)) insertionsort#(l) -> c_29(insertionsort'1#(l)) insertionsort'1#(dd(x,xs)) -> c_30(insert#(x,insertionsort(xs)),insertionsort#(xs)) - Weak TRS: 'cklt('EQ()) -> 'false() 'cklt('GT()) -> 'false() 'cklt('LT()) -> 'true() 'compare('0(),'0()) -> 'EQ() 'compare('0(),'neg(y)) -> 'GT() 'compare('0(),'pos(y)) -> 'LT() 'compare('0(),'s(y)) -> 'LT() 'compare('neg(x),'0()) -> 'LT() 'compare('neg(x),'neg(y)) -> 'compare(y,x) 'compare('neg(x),'pos(y)) -> 'LT() 'compare('pos(x),'0()) -> 'GT() 'compare('pos(x),'neg(y)) -> 'GT() 'compare('pos(x),'pos(y)) -> 'compare(x,y) 'compare('s(x),'0()) -> 'GT() 'compare('s(x),'s(y)) -> 'compare(x,y) 'less(x,y) -> 'cklt('compare(x,y)) append(l1,l2) -> append'1(l1,l2) append'1(dd(x,xs),l2) -> dd(x,append(xs,l2)) append'1(nil(),l2) -> l2 flatten(t) -> flatten'1(t) flatten'1(leaf()) -> nil() flatten'1(node(l,t1,t2)) -> append(l,append(flatten(t1),flatten(t2))) insert(x,l) -> insert'1(l,x) insert'1(dd(y,ys),x) -> insert'2('less(y,x),x,y,ys) insert'1(nil(),x) -> dd(x,nil()) insert'2('false(),x,y,ys) -> dd(x,dd(y,ys)) insert'2('true(),x,y,ys) -> dd(y,insert(x,ys)) insertionsort(l) -> insertionsort'1(l) insertionsort'1(dd(x,xs)) -> insert(x,insertionsort(xs)) insertionsort'1(nil()) -> nil() - Signature: {'cklt/1,'compare/2,'less/2,append/2,append'1/2,flatten/1,flatten'1/1,flattensort/1,insert/2,insert'1/2 ,insert'2/4,insertionsort/1,insertionsort'1/1,'cklt#/1,'compare#/2,'less#/2,append#/2,append'1#/2,flatten#/1 ,flatten'1#/1,flattensort#/1,insert#/2,insert'1#/2,insert'2#/4,insertionsort#/1,insertionsort'1#/1} / {'0/0 ,'EQ/0,'GT/0,'LT/0,'false/0,'neg/1,'pos/1,'s/1,'true/0,dd/2,leaf/0,nil/0,node/3,c_1/0,c_2/0,c_3/0,c_4/0 ,c_5/0,c_6/0,c_7/0,c_8/0,c_9/1,c_10/0,c_11/0,c_12/0,c_13/1,c_14/0,c_15/1,c_16/1,c_17/1,c_18/1,c_19/0,c_20/1 ,c_21/0,c_22/4,c_23/2,c_24/1,c_25/2,c_26/0,c_27/0,c_28/1,c_29/1,c_30/2,c_31/0} - Obligation: innermost runtime complexity wrt. defined symbols {'cklt#,'compare#,'less#,append#,append'1#,flatten# ,flatten'1#,flattensort#,insert#,insert'1#,insert'2#,insertionsort#,insertionsort'1#} and constructors {'0 ,'EQ,'GT,'LT,'false,'neg,'pos,'s,'true,dd,leaf,nil,node} + Applied Processor: SimplifyRHS + Details: Consider the dependency graph 1:S:flatten#(t) -> c_20(flatten'1#(t)) -->_1 flatten'1#(node(l,t1,t2)) -> c_22(append#(l,append(flatten(t1),flatten(t2))) ,append#(flatten(t1),flatten(t2)) ,flatten#(t1) ,flatten#(t2)):2 2:S:flatten'1#(node(l,t1,t2)) -> c_22(append#(l,append(flatten(t1),flatten(t2))) ,append#(flatten(t1),flatten(t2)) ,flatten#(t1) ,flatten#(t2)) -->_4 flatten#(t) -> c_20(flatten'1#(t)):1 -->_3 flatten#(t) -> c_20(flatten'1#(t)):1 3:S:flattensort#(t) -> c_23(insertionsort#(flatten(t)),flatten#(t)) -->_1 insertionsort#(l) -> c_29(insertionsort'1#(l)):4 -->_2 flatten#(t) -> c_20(flatten'1#(t)):1 4:S:insertionsort#(l) -> c_29(insertionsort'1#(l)) -->_1 insertionsort'1#(dd(x,xs)) -> c_30(insert#(x,insertionsort(xs)),insertionsort#(xs)):5 5:S:insertionsort'1#(dd(x,xs)) -> c_30(insert#(x,insertionsort(xs)),insertionsort#(xs)) -->_2 insertionsort#(l) -> c_29(insertionsort'1#(l)):4 Due to missing edges in the depndency graph, the right-hand sides of following rules could be simplified: flatten'1#(node(l,t1,t2)) -> c_22(flatten#(t1),flatten#(t2)) insertionsort'1#(dd(x,xs)) -> c_30(insertionsort#(xs)) ** Step 6.a:2: UsableRules WORST_CASE(?,O(n^1)) + Considered Problem: - Strict DPs: flatten#(t) -> c_20(flatten'1#(t)) flatten'1#(node(l,t1,t2)) -> c_22(flatten#(t1),flatten#(t2)) flattensort#(t) -> c_23(insertionsort#(flatten(t)),flatten#(t)) insertionsort#(l) -> c_29(insertionsort'1#(l)) insertionsort'1#(dd(x,xs)) -> c_30(insertionsort#(xs)) - Weak TRS: 'cklt('EQ()) -> 'false() 'cklt('GT()) -> 'false() 'cklt('LT()) -> 'true() 'compare('0(),'0()) -> 'EQ() 'compare('0(),'neg(y)) -> 'GT() 'compare('0(),'pos(y)) -> 'LT() 'compare('0(),'s(y)) -> 'LT() 'compare('neg(x),'0()) -> 'LT() 'compare('neg(x),'neg(y)) -> 'compare(y,x) 'compare('neg(x),'pos(y)) -> 'LT() 'compare('pos(x),'0()) -> 'GT() 'compare('pos(x),'neg(y)) -> 'GT() 'compare('pos(x),'pos(y)) -> 'compare(x,y) 'compare('s(x),'0()) -> 'GT() 'compare('s(x),'s(y)) -> 'compare(x,y) 'less(x,y) -> 'cklt('compare(x,y)) append(l1,l2) -> append'1(l1,l2) append'1(dd(x,xs),l2) -> dd(x,append(xs,l2)) append'1(nil(),l2) -> l2 flatten(t) -> flatten'1(t) flatten'1(leaf()) -> nil() flatten'1(node(l,t1,t2)) -> append(l,append(flatten(t1),flatten(t2))) insert(x,l) -> insert'1(l,x) insert'1(dd(y,ys),x) -> insert'2('less(y,x),x,y,ys) insert'1(nil(),x) -> dd(x,nil()) insert'2('false(),x,y,ys) -> dd(x,dd(y,ys)) insert'2('true(),x,y,ys) -> dd(y,insert(x,ys)) insertionsort(l) -> insertionsort'1(l) insertionsort'1(dd(x,xs)) -> insert(x,insertionsort(xs)) insertionsort'1(nil()) -> nil() - Signature: {'cklt/1,'compare/2,'less/2,append/2,append'1/2,flatten/1,flatten'1/1,flattensort/1,insert/2,insert'1/2 ,insert'2/4,insertionsort/1,insertionsort'1/1,'cklt#/1,'compare#/2,'less#/2,append#/2,append'1#/2,flatten#/1 ,flatten'1#/1,flattensort#/1,insert#/2,insert'1#/2,insert'2#/4,insertionsort#/1,insertionsort'1#/1} / {'0/0 ,'EQ/0,'GT/0,'LT/0,'false/0,'neg/1,'pos/1,'s/1,'true/0,dd/2,leaf/0,nil/0,node/3,c_1/0,c_2/0,c_3/0,c_4/0 ,c_5/0,c_6/0,c_7/0,c_8/0,c_9/1,c_10/0,c_11/0,c_12/0,c_13/1,c_14/0,c_15/1,c_16/1,c_17/1,c_18/1,c_19/0,c_20/1 ,c_21/0,c_22/2,c_23/2,c_24/1,c_25/2,c_26/0,c_27/0,c_28/1,c_29/1,c_30/1,c_31/0} - Obligation: innermost runtime complexity wrt. defined symbols {'cklt#,'compare#,'less#,append#,append'1#,flatten# ,flatten'1#,flattensort#,insert#,insert'1#,insert'2#,insertionsort#,insertionsort'1#} and constructors {'0 ,'EQ,'GT,'LT,'false,'neg,'pos,'s,'true,dd,leaf,nil,node} + Applied Processor: UsableRules + Details: We replace rewrite rules by usable rules: append(l1,l2) -> append'1(l1,l2) append'1(dd(x,xs),l2) -> dd(x,append(xs,l2)) append'1(nil(),l2) -> l2 flatten(t) -> flatten'1(t) flatten'1(leaf()) -> nil() flatten'1(node(l,t1,t2)) -> append(l,append(flatten(t1),flatten(t2))) flatten#(t) -> c_20(flatten'1#(t)) flatten'1#(node(l,t1,t2)) -> c_22(flatten#(t1),flatten#(t2)) flattensort#(t) -> c_23(insertionsort#(flatten(t)),flatten#(t)) insertionsort#(l) -> c_29(insertionsort'1#(l)) insertionsort'1#(dd(x,xs)) -> c_30(insertionsort#(xs)) ** Step 6.a:3: Ara WORST_CASE(?,O(n^1)) + Considered Problem: - Strict DPs: flatten#(t) -> c_20(flatten'1#(t)) flatten'1#(node(l,t1,t2)) -> c_22(flatten#(t1),flatten#(t2)) flattensort#(t) -> c_23(insertionsort#(flatten(t)),flatten#(t)) insertionsort#(l) -> c_29(insertionsort'1#(l)) insertionsort'1#(dd(x,xs)) -> c_30(insertionsort#(xs)) - Weak TRS: append(l1,l2) -> append'1(l1,l2) append'1(dd(x,xs),l2) -> dd(x,append(xs,l2)) append'1(nil(),l2) -> l2 flatten(t) -> flatten'1(t) flatten'1(leaf()) -> nil() flatten'1(node(l,t1,t2)) -> append(l,append(flatten(t1),flatten(t2))) - Signature: {'cklt/1,'compare/2,'less/2,append/2,append'1/2,flatten/1,flatten'1/1,flattensort/1,insert/2,insert'1/2 ,insert'2/4,insertionsort/1,insertionsort'1/1,'cklt#/1,'compare#/2,'less#/2,append#/2,append'1#/2,flatten#/1 ,flatten'1#/1,flattensort#/1,insert#/2,insert'1#/2,insert'2#/4,insertionsort#/1,insertionsort'1#/1} / {'0/0 ,'EQ/0,'GT/0,'LT/0,'false/0,'neg/1,'pos/1,'s/1,'true/0,dd/2,leaf/0,nil/0,node/3,c_1/0,c_2/0,c_3/0,c_4/0 ,c_5/0,c_6/0,c_7/0,c_8/0,c_9/1,c_10/0,c_11/0,c_12/0,c_13/1,c_14/0,c_15/1,c_16/1,c_17/1,c_18/1,c_19/0,c_20/1 ,c_21/0,c_22/2,c_23/2,c_24/1,c_25/2,c_26/0,c_27/0,c_28/1,c_29/1,c_30/1,c_31/0} - Obligation: innermost runtime complexity wrt. defined symbols {'cklt#,'compare#,'less#,append#,append'1#,flatten# ,flatten'1#,flattensort#,insert#,insert'1#,insert'2#,insertionsort#,insertionsort'1#} and constructors {'0 ,'EQ,'GT,'LT,'false,'neg,'pos,'s,'true,dd,leaf,nil,node} + Applied Processor: Ara {araHeuristics = NoHeuristics, minDegree = 1, maxDegree = 2, araTimeout = 8, araRuleShifting = Just 1} + Details: Signatures used: ---------------- append :: ["A"(0) x "A"(0)] -(0)-> "A"(0) append'1 :: ["A"(0) x "A"(0)] -(0)-> "A"(0) dd :: ["A"(0) x "A"(0)] -(0)-> "A"(0) flatten :: ["A"(0)] -(0)-> "A"(0) flatten'1 :: ["A"(0)] -(0)-> "A"(0) leaf :: [] -(0)-> "A"(0) nil :: [] -(0)-> "A"(0) node :: ["A"(0) x "A"(0) x "A"(0)] -(0)-> "A"(0) flatten# :: ["A"(0)] -(0)-> "A"(0) flatten'1# :: ["A"(0)] -(0)-> "A"(0) flattensort# :: ["A"(0)] -(1)-> "A"(0) insertionsort# :: ["A"(0)] -(0)-> "A"(0) insertionsort'1# :: ["A"(0)] -(0)-> "A"(0) c_20 :: ["A"(0)] -(0)-> "A"(0) c_22 :: ["A"(0) x "A"(0)] -(0)-> "A"(0) c_23 :: ["A"(0) x "A"(0)] -(0)-> "A"(0) c_29 :: ["A"(0)] -(0)-> "A"(0) c_30 :: ["A"(0)] -(0)-> "A"(0) Cost-free Signatures used: -------------------------- Base Constructor Signatures used: --------------------------------- Following Still Strict Rules were Typed as: ------------------------------------------- 1. Strict: flattensort#(t) -> c_23(insertionsort#(flatten(t)),flatten#(t)) 2. Weak: flatten#(t) -> c_20(flatten'1#(t)) flatten'1#(node(l,t1,t2)) -> c_22(flatten#(t1),flatten#(t2)) insertionsort#(l) -> c_29(insertionsort'1#(l)) insertionsort'1#(dd(x,xs)) -> c_30(insertionsort#(xs)) ** Step 6.a:4: Ara WORST_CASE(?,O(n^1)) + Considered Problem: - Strict DPs: flatten#(t) -> c_20(flatten'1#(t)) flatten'1#(node(l,t1,t2)) -> c_22(flatten#(t1),flatten#(t2)) insertionsort#(l) -> c_29(insertionsort'1#(l)) insertionsort'1#(dd(x,xs)) -> c_30(insertionsort#(xs)) - Weak DPs: flattensort#(t) -> c_23(insertionsort#(flatten(t)),flatten#(t)) - Weak TRS: append(l1,l2) -> append'1(l1,l2) append'1(dd(x,xs),l2) -> dd(x,append(xs,l2)) append'1(nil(),l2) -> l2 flatten(t) -> flatten'1(t) flatten'1(leaf()) -> nil() flatten'1(node(l,t1,t2)) -> append(l,append(flatten(t1),flatten(t2))) - Signature: {'cklt/1,'compare/2,'less/2,append/2,append'1/2,flatten/1,flatten'1/1,flattensort/1,insert/2,insert'1/2 ,insert'2/4,insertionsort/1,insertionsort'1/1,'cklt#/1,'compare#/2,'less#/2,append#/2,append'1#/2,flatten#/1 ,flatten'1#/1,flattensort#/1,insert#/2,insert'1#/2,insert'2#/4,insertionsort#/1,insertionsort'1#/1} / {'0/0 ,'EQ/0,'GT/0,'LT/0,'false/0,'neg/1,'pos/1,'s/1,'true/0,dd/2,leaf/0,nil/0,node/3,c_1/0,c_2/0,c_3/0,c_4/0 ,c_5/0,c_6/0,c_7/0,c_8/0,c_9/1,c_10/0,c_11/0,c_12/0,c_13/1,c_14/0,c_15/1,c_16/1,c_17/1,c_18/1,c_19/0,c_20/1 ,c_21/0,c_22/2,c_23/2,c_24/1,c_25/2,c_26/0,c_27/0,c_28/1,c_29/1,c_30/1,c_31/0} - Obligation: innermost runtime complexity wrt. defined symbols {'cklt#,'compare#,'less#,append#,append'1#,flatten# ,flatten'1#,flattensort#,insert#,insert'1#,insert'2#,insertionsort#,insertionsort'1#} and constructors {'0 ,'EQ,'GT,'LT,'false,'neg,'pos,'s,'true,dd,leaf,nil,node} + Applied Processor: Ara {araHeuristics = NoHeuristics, minDegree = 1, maxDegree = 2, araTimeout = 8, araRuleShifting = Just 1} + Details: Signatures used: ---------------- append :: ["A"(0) x "A"(5)] -(0)-> "A"(5) append'1 :: ["A"(0) x "A"(5)] -(0)-> "A"(5) dd :: ["A"(0) x "A"(4)] -(0)-> "A"(4) dd :: ["A"(0) x "A"(0)] -(0)-> "A"(0) dd :: ["A"(0) x "A"(5)] -(0)-> "A"(5) flatten :: ["A"(3)] -(1)-> "A"(5) flatten'1 :: ["A"(3)] -(1)-> "A"(5) leaf :: [] -(0)-> "A"(3) nil :: [] -(0)-> "A"(0) nil :: [] -(0)-> "A"(11) node :: ["A"(12) x "A"(12) x "A"(12)] -(12)-> "A"(12) node :: ["A"(3) x "A"(3) x "A"(3)] -(3)-> "A"(3) flatten# :: ["A"(12)] -(2)-> "A"(1) flatten'1# :: ["A"(12)] -(0)-> "A"(1) flattensort# :: ["A"(15)] -(15)-> "A"(0) insertionsort# :: ["A"(4)] -(7)-> "A"(1) insertionsort'1# :: ["A"(4)] -(7)-> "A"(4) c_20 :: ["A"(1)] -(0)-> "A"(1) c_22 :: ["A"(1) x "A"(1)] -(0)-> "A"(1) c_23 :: ["A"(1) x "A"(1)] -(0)-> "A"(1) c_29 :: ["A"(0)] -(0)-> "A"(12) c_30 :: ["A"(0)] -(0)-> "A"(7) Cost-free Signatures used: -------------------------- Base Constructor Signatures used: --------------------------------- "c_20_A" :: ["A"(0)] -(0)-> "A"(1) "c_22_A" :: ["A"(0) x "A"(0)] -(0)-> "A"(1) "c_23_A" :: ["A"(0) x "A"(0)] -(0)-> "A"(1) "c_29_A" :: ["A"(0)] -(0)-> "A"(1) "c_30_A" :: ["A"(0)] -(0)-> "A"(1) "dd_A" :: ["A"(0) x "A"(1)] -(0)-> "A"(1) "leaf_A" :: [] -(0)-> "A"(1) "nil_A" :: [] -(0)-> "A"(1) "node_A" :: ["A"(1) x "A"(1) x "A"(1)] -(1)-> "A"(1) Following Still Strict Rules were Typed as: ------------------------------------------- 1. Strict: flatten'1#(node(l,t1,t2)) -> c_22(flatten#(t1),flatten#(t2)) 2. Weak: flatten#(t) -> c_20(flatten'1#(t)) insertionsort#(l) -> c_29(insertionsort'1#(l)) insertionsort'1#(dd(x,xs)) -> c_30(insertionsort#(xs)) ** Step 6.a:5: Ara WORST_CASE(?,O(n^1)) + Considered Problem: - Strict DPs: flatten#(t) -> c_20(flatten'1#(t)) insertionsort#(l) -> c_29(insertionsort'1#(l)) insertionsort'1#(dd(x,xs)) -> c_30(insertionsort#(xs)) - Weak DPs: flatten'1#(node(l,t1,t2)) -> c_22(flatten#(t1),flatten#(t2)) flattensort#(t) -> c_23(insertionsort#(flatten(t)),flatten#(t)) - Weak TRS: append(l1,l2) -> append'1(l1,l2) append'1(dd(x,xs),l2) -> dd(x,append(xs,l2)) append'1(nil(),l2) -> l2 flatten(t) -> flatten'1(t) flatten'1(leaf()) -> nil() flatten'1(node(l,t1,t2)) -> append(l,append(flatten(t1),flatten(t2))) - Signature: {'cklt/1,'compare/2,'less/2,append/2,append'1/2,flatten/1,flatten'1/1,flattensort/1,insert/2,insert'1/2 ,insert'2/4,insertionsort/1,insertionsort'1/1,'cklt#/1,'compare#/2,'less#/2,append#/2,append'1#/2,flatten#/1 ,flatten'1#/1,flattensort#/1,insert#/2,insert'1#/2,insert'2#/4,insertionsort#/1,insertionsort'1#/1} / {'0/0 ,'EQ/0,'GT/0,'LT/0,'false/0,'neg/1,'pos/1,'s/1,'true/0,dd/2,leaf/0,nil/0,node/3,c_1/0,c_2/0,c_3/0,c_4/0 ,c_5/0,c_6/0,c_7/0,c_8/0,c_9/1,c_10/0,c_11/0,c_12/0,c_13/1,c_14/0,c_15/1,c_16/1,c_17/1,c_18/1,c_19/0,c_20/1 ,c_21/0,c_22/2,c_23/2,c_24/1,c_25/2,c_26/0,c_27/0,c_28/1,c_29/1,c_30/1,c_31/0} - Obligation: innermost runtime complexity wrt. defined symbols {'cklt#,'compare#,'less#,append#,append'1#,flatten# ,flatten'1#,flattensort#,insert#,insert'1#,insert'2#,insertionsort#,insertionsort'1#} and constructors {'0 ,'EQ,'GT,'LT,'false,'neg,'pos,'s,'true,dd,leaf,nil,node} + Applied Processor: Ara {araHeuristics = NoHeuristics, minDegree = 1, maxDegree = 2, araTimeout = 8, araRuleShifting = Just 1} + Details: Signatures used: ---------------- append :: ["A"(9) x "A"(9)] -(1)-> "A"(9) append'1 :: ["A"(9) x "A"(9)] -(1)-> "A"(9) dd :: ["A"(7) x "A"(7)] -(7)-> "A"(7) dd :: ["A"(9) x "A"(9)] -(9)-> "A"(9) flatten :: ["A"(15)] -(3)-> "A"(9) flatten'1 :: ["A"(15)] -(3)-> "A"(9) leaf :: [] -(0)-> "A"(15) nil :: [] -(0)-> "A"(9) nil :: [] -(0)-> "A"(14) node :: ["A"(15) x "A"(15) x "A"(15)] -(15)-> "A"(15) node :: ["A"(0) x "A"(0) x "A"(0)] -(0)-> "A"(0) flatten# :: ["A"(0)] -(0)-> "A"(6) flatten'1# :: ["A"(0)] -(0)-> "A"(8) flattensort# :: ["A"(15)] -(15)-> "A"(0) insertionsort# :: ["A"(7)] -(7)-> "A"(2) insertionsort'1# :: ["A"(7)] -(3)-> "A"(14) c_20 :: ["A"(6)] -(0)-> "A"(6) c_22 :: ["A"(0) x "A"(0)] -(0)-> "A"(12) c_23 :: ["A"(0) x "A"(6)] -(0)-> "A"(6) c_29 :: ["A"(12)] -(0)-> "A"(12) c_30 :: ["A"(0)] -(0)-> "A"(14) Cost-free Signatures used: -------------------------- Base Constructor Signatures used: --------------------------------- "c_20_A" :: ["A"(0)] -(0)-> "A"(1) "c_22_A" :: ["A"(0) x "A"(0)] -(0)-> "A"(1) "c_23_A" :: ["A"(0) x "A"(0)] -(0)-> "A"(1) "c_29_A" :: ["A"(0)] -(0)-> "A"(1) "c_30_A" :: ["A"(0)] -(0)-> "A"(1) "dd_A" :: ["A"(1) x "A"(1)] -(1)-> "A"(1) "leaf_A" :: [] -(0)-> "A"(1) "nil_A" :: [] -(0)-> "A"(1) "node_A" :: ["A"(1) x "A"(1) x "A"(1)] -(1)-> "A"(1) Following Still Strict Rules were Typed as: ------------------------------------------- 1. Strict: insertionsort#(l) -> c_29(insertionsort'1#(l)) insertionsort'1#(dd(x,xs)) -> c_30(insertionsort#(xs)) 2. Weak: flatten#(t) -> c_20(flatten'1#(t)) ** Step 6.a:6: Ara WORST_CASE(?,O(n^1)) + Considered Problem: - Strict DPs: flatten#(t) -> c_20(flatten'1#(t)) - Weak DPs: flatten'1#(node(l,t1,t2)) -> c_22(flatten#(t1),flatten#(t2)) flattensort#(t) -> c_23(insertionsort#(flatten(t)),flatten#(t)) insertionsort#(l) -> c_29(insertionsort'1#(l)) insertionsort'1#(dd(x,xs)) -> c_30(insertionsort#(xs)) - Weak TRS: append(l1,l2) -> append'1(l1,l2) append'1(dd(x,xs),l2) -> dd(x,append(xs,l2)) append'1(nil(),l2) -> l2 flatten(t) -> flatten'1(t) flatten'1(leaf()) -> nil() flatten'1(node(l,t1,t2)) -> append(l,append(flatten(t1),flatten(t2))) - Signature: {'cklt/1,'compare/2,'less/2,append/2,append'1/2,flatten/1,flatten'1/1,flattensort/1,insert/2,insert'1/2 ,insert'2/4,insertionsort/1,insertionsort'1/1,'cklt#/1,'compare#/2,'less#/2,append#/2,append'1#/2,flatten#/1 ,flatten'1#/1,flattensort#/1,insert#/2,insert'1#/2,insert'2#/4,insertionsort#/1,insertionsort'1#/1} / {'0/0 ,'EQ/0,'GT/0,'LT/0,'false/0,'neg/1,'pos/1,'s/1,'true/0,dd/2,leaf/0,nil/0,node/3,c_1/0,c_2/0,c_3/0,c_4/0 ,c_5/0,c_6/0,c_7/0,c_8/0,c_9/1,c_10/0,c_11/0,c_12/0,c_13/1,c_14/0,c_15/1,c_16/1,c_17/1,c_18/1,c_19/0,c_20/1 ,c_21/0,c_22/2,c_23/2,c_24/1,c_25/2,c_26/0,c_27/0,c_28/1,c_29/1,c_30/1,c_31/0} - Obligation: innermost runtime complexity wrt. defined symbols {'cklt#,'compare#,'less#,append#,append'1#,flatten# ,flatten'1#,flattensort#,insert#,insert'1#,insert'2#,insertionsort#,insertionsort'1#} and constructors {'0 ,'EQ,'GT,'LT,'false,'neg,'pos,'s,'true,dd,leaf,nil,node} + Applied Processor: Ara {araHeuristics = NoHeuristics, minDegree = 1, maxDegree = 2, araTimeout = 8, araRuleShifting = Just 1} + Details: Signatures used: ---------------- append :: ["A"(0) x "A"(14)] -(0)-> "A"(14) append'1 :: ["A"(0) x "A"(14)] -(0)-> "A"(14) dd :: ["A"(0) x "A"(0)] -(0)-> "A"(0) dd :: ["A"(0) x "A"(12)] -(0)-> "A"(12) dd :: ["A"(0) x "A"(14)] -(0)-> "A"(14) flatten :: ["A"(0)] -(0)-> "A"(14) flatten'1 :: ["A"(0)] -(0)-> "A"(14) leaf :: [] -(0)-> "A"(0) nil :: [] -(0)-> "A"(0) nil :: [] -(0)-> "A"(14) node :: ["A"(0) x "A"(0) x "A"(0)] -(0)-> "A"(0) node :: ["A"(0) x "A"(15) x "A"(15)] -(15)-> "A"(15) flatten# :: ["A"(15)] -(4)-> "A"(0) flatten'1# :: ["A"(15)] -(3)-> "A"(14) flattensort# :: ["A"(15)] -(15)-> "A"(0) insertionsort# :: ["A"(12)] -(0)-> "A"(3) insertionsort'1# :: ["A"(12)] -(0)-> "A"(5) c_20 :: ["A"(0)] -(0)-> "A"(0) c_22 :: ["A"(0) x "A"(0)] -(0)-> "A"(14) c_23 :: ["A"(0) x "A"(0)] -(0)-> "A"(6) c_29 :: ["A"(0)] -(0)-> "A"(13) c_30 :: ["A"(0)] -(0)-> "A"(6) Cost-free Signatures used: -------------------------- Base Constructor Signatures used: --------------------------------- "c_20_A" :: ["A"(0)] -(0)-> "A"(1) "c_22_A" :: ["A"(0) x "A"(0)] -(0)-> "A"(1) "c_23_A" :: ["A"(0) x "A"(0)] -(0)-> "A"(1) "c_29_A" :: ["A"(0)] -(0)-> "A"(1) "c_30_A" :: ["A"(0)] -(0)-> "A"(1) "dd_A" :: ["A"(0) x "A"(1)] -(0)-> "A"(1) "leaf_A" :: [] -(0)-> "A"(1) "nil_A" :: [] -(0)-> "A"(1) "node_A" :: ["A"(0) x "A"(1) x "A"(1)] -(1)-> "A"(1) Following Still Strict Rules were Typed as: ------------------------------------------- 1. Strict: flatten#(t) -> c_20(flatten'1#(t)) 2. Weak: ** Step 6.b:1: DecomposeDG WORST_CASE(?,O(n^2)) + Considered Problem: - Strict DPs: 'compare#('neg(x),'neg(y)) -> c_9('compare#(y,x)) 'compare#('pos(x),'pos(y)) -> c_13('compare#(x,y)) 'compare#('s(x),'s(y)) -> c_15('compare#(x,y)) 'less#(x,y) -> c_16('compare#(x,y)) append#(l1,l2) -> c_17(append'1#(l1,l2)) append'1#(dd(x,xs),l2) -> c_18(append#(xs,l2)) insert#(x,l) -> c_24(insert'1#(l,x)) insert'1#(dd(y,ys),x) -> c_25(insert'2#('less(y,x),x,y,ys),'less#(y,x)) insert'2#('true(),x,y,ys) -> c_28(insert#(x,ys)) - Weak DPs: flatten#(t) -> flatten'1#(t) flatten'1#(node(l,t1,t2)) -> append#(l,append(flatten(t1),flatten(t2))) flatten'1#(node(l,t1,t2)) -> append#(flatten(t1),flatten(t2)) flatten'1#(node(l,t1,t2)) -> flatten#(t1) flatten'1#(node(l,t1,t2)) -> flatten#(t2) flattensort#(t) -> flatten#(t) flattensort#(t) -> insertionsort#(flatten(t)) insertionsort#(l) -> insertionsort'1#(l) insertionsort'1#(dd(x,xs)) -> insert#(x,insertionsort(xs)) insertionsort'1#(dd(x,xs)) -> insertionsort#(xs) - Weak TRS: 'cklt('EQ()) -> 'false() 'cklt('GT()) -> 'false() 'cklt('LT()) -> 'true() 'compare('0(),'0()) -> 'EQ() 'compare('0(),'neg(y)) -> 'GT() 'compare('0(),'pos(y)) -> 'LT() 'compare('0(),'s(y)) -> 'LT() 'compare('neg(x),'0()) -> 'LT() 'compare('neg(x),'neg(y)) -> 'compare(y,x) 'compare('neg(x),'pos(y)) -> 'LT() 'compare('pos(x),'0()) -> 'GT() 'compare('pos(x),'neg(y)) -> 'GT() 'compare('pos(x),'pos(y)) -> 'compare(x,y) 'compare('s(x),'0()) -> 'GT() 'compare('s(x),'s(y)) -> 'compare(x,y) 'less(x,y) -> 'cklt('compare(x,y)) append(l1,l2) -> append'1(l1,l2) append'1(dd(x,xs),l2) -> dd(x,append(xs,l2)) append'1(nil(),l2) -> l2 flatten(t) -> flatten'1(t) flatten'1(leaf()) -> nil() flatten'1(node(l,t1,t2)) -> append(l,append(flatten(t1),flatten(t2))) insert(x,l) -> insert'1(l,x) insert'1(dd(y,ys),x) -> insert'2('less(y,x),x,y,ys) insert'1(nil(),x) -> dd(x,nil()) insert'2('false(),x,y,ys) -> dd(x,dd(y,ys)) insert'2('true(),x,y,ys) -> dd(y,insert(x,ys)) insertionsort(l) -> insertionsort'1(l) insertionsort'1(dd(x,xs)) -> insert(x,insertionsort(xs)) insertionsort'1(nil()) -> nil() - Signature: {'cklt/1,'compare/2,'less/2,append/2,append'1/2,flatten/1,flatten'1/1,flattensort/1,insert/2,insert'1/2 ,insert'2/4,insertionsort/1,insertionsort'1/1,'cklt#/1,'compare#/2,'less#/2,append#/2,append'1#/2,flatten#/1 ,flatten'1#/1,flattensort#/1,insert#/2,insert'1#/2,insert'2#/4,insertionsort#/1,insertionsort'1#/1} / {'0/0 ,'EQ/0,'GT/0,'LT/0,'false/0,'neg/1,'pos/1,'s/1,'true/0,dd/2,leaf/0,nil/0,node/3,c_1/0,c_2/0,c_3/0,c_4/0 ,c_5/0,c_6/0,c_7/0,c_8/0,c_9/1,c_10/0,c_11/0,c_12/0,c_13/1,c_14/0,c_15/1,c_16/1,c_17/1,c_18/1,c_19/0,c_20/1 ,c_21/0,c_22/4,c_23/2,c_24/1,c_25/2,c_26/0,c_27/0,c_28/1,c_29/1,c_30/2,c_31/0} - Obligation: innermost runtime complexity wrt. defined symbols {'cklt#,'compare#,'less#,append#,append'1#,flatten# ,flatten'1#,flattensort#,insert#,insert'1#,insert'2#,insertionsort#,insertionsort'1#} and constructors {'0 ,'EQ,'GT,'LT,'false,'neg,'pos,'s,'true,dd,leaf,nil,node} + Applied Processor: DecomposeDG {onSelection = all below first cut in WDG, onUpper = Nothing, onLower = Nothing} + Details: We decompose the input problem according to the dependency graph into the upper component append#(l1,l2) -> c_17(append'1#(l1,l2)) append'1#(dd(x,xs),l2) -> c_18(append#(xs,l2)) flatten#(t) -> flatten'1#(t) flatten'1#(node(l,t1,t2)) -> append#(l,append(flatten(t1),flatten(t2))) flatten'1#(node(l,t1,t2)) -> append#(flatten(t1),flatten(t2)) flatten'1#(node(l,t1,t2)) -> flatten#(t1) flatten'1#(node(l,t1,t2)) -> flatten#(t2) flattensort#(t) -> flatten#(t) flattensort#(t) -> insertionsort#(flatten(t)) insert#(x,l) -> c_24(insert'1#(l,x)) insert'1#(dd(y,ys),x) -> c_25(insert'2#('less(y,x),x,y,ys),'less#(y,x)) insert'2#('true(),x,y,ys) -> c_28(insert#(x,ys)) insertionsort#(l) -> insertionsort'1#(l) insertionsort'1#(dd(x,xs)) -> insert#(x,insertionsort(xs)) insertionsort'1#(dd(x,xs)) -> insertionsort#(xs) and a lower component 'compare#('neg(x),'neg(y)) -> c_9('compare#(y,x)) 'compare#('pos(x),'pos(y)) -> c_13('compare#(x,y)) 'compare#('s(x),'s(y)) -> c_15('compare#(x,y)) 'less#(x,y) -> c_16('compare#(x,y)) Further, following extension rules are added to the lower component. append#(l1,l2) -> append'1#(l1,l2) append'1#(dd(x,xs),l2) -> append#(xs,l2) flatten#(t) -> flatten'1#(t) flatten'1#(node(l,t1,t2)) -> append#(l,append(flatten(t1),flatten(t2))) flatten'1#(node(l,t1,t2)) -> append#(flatten(t1),flatten(t2)) flatten'1#(node(l,t1,t2)) -> flatten#(t1) flatten'1#(node(l,t1,t2)) -> flatten#(t2) flattensort#(t) -> flatten#(t) flattensort#(t) -> insertionsort#(flatten(t)) insert#(x,l) -> insert'1#(l,x) insert'1#(dd(y,ys),x) -> 'less#(y,x) insert'1#(dd(y,ys),x) -> insert'2#('less(y,x),x,y,ys) insert'2#('true(),x,y,ys) -> insert#(x,ys) insertionsort#(l) -> insertionsort'1#(l) insertionsort'1#(dd(x,xs)) -> insert#(x,insertionsort(xs)) insertionsort'1#(dd(x,xs)) -> insertionsort#(xs) *** Step 6.b:1.a:1: RemoveHeads WORST_CASE(?,O(n^1)) + Considered Problem: - Strict DPs: append#(l1,l2) -> c_17(append'1#(l1,l2)) append'1#(dd(x,xs),l2) -> c_18(append#(xs,l2)) insert#(x,l) -> c_24(insert'1#(l,x)) insert'1#(dd(y,ys),x) -> c_25(insert'2#('less(y,x),x,y,ys),'less#(y,x)) insert'2#('true(),x,y,ys) -> c_28(insert#(x,ys)) - Weak DPs: flatten#(t) -> flatten'1#(t) flatten'1#(node(l,t1,t2)) -> append#(l,append(flatten(t1),flatten(t2))) flatten'1#(node(l,t1,t2)) -> append#(flatten(t1),flatten(t2)) flatten'1#(node(l,t1,t2)) -> flatten#(t1) flatten'1#(node(l,t1,t2)) -> flatten#(t2) flattensort#(t) -> flatten#(t) flattensort#(t) -> insertionsort#(flatten(t)) insertionsort#(l) -> insertionsort'1#(l) insertionsort'1#(dd(x,xs)) -> insert#(x,insertionsort(xs)) insertionsort'1#(dd(x,xs)) -> insertionsort#(xs) - Weak TRS: 'cklt('EQ()) -> 'false() 'cklt('GT()) -> 'false() 'cklt('LT()) -> 'true() 'compare('0(),'0()) -> 'EQ() 'compare('0(),'neg(y)) -> 'GT() 'compare('0(),'pos(y)) -> 'LT() 'compare('0(),'s(y)) -> 'LT() 'compare('neg(x),'0()) -> 'LT() 'compare('neg(x),'neg(y)) -> 'compare(y,x) 'compare('neg(x),'pos(y)) -> 'LT() 'compare('pos(x),'0()) -> 'GT() 'compare('pos(x),'neg(y)) -> 'GT() 'compare('pos(x),'pos(y)) -> 'compare(x,y) 'compare('s(x),'0()) -> 'GT() 'compare('s(x),'s(y)) -> 'compare(x,y) 'less(x,y) -> 'cklt('compare(x,y)) append(l1,l2) -> append'1(l1,l2) append'1(dd(x,xs),l2) -> dd(x,append(xs,l2)) append'1(nil(),l2) -> l2 flatten(t) -> flatten'1(t) flatten'1(leaf()) -> nil() flatten'1(node(l,t1,t2)) -> append(l,append(flatten(t1),flatten(t2))) insert(x,l) -> insert'1(l,x) insert'1(dd(y,ys),x) -> insert'2('less(y,x),x,y,ys) insert'1(nil(),x) -> dd(x,nil()) insert'2('false(),x,y,ys) -> dd(x,dd(y,ys)) insert'2('true(),x,y,ys) -> dd(y,insert(x,ys)) insertionsort(l) -> insertionsort'1(l) insertionsort'1(dd(x,xs)) -> insert(x,insertionsort(xs)) insertionsort'1(nil()) -> nil() - Signature: {'cklt/1,'compare/2,'less/2,append/2,append'1/2,flatten/1,flatten'1/1,flattensort/1,insert/2,insert'1/2 ,insert'2/4,insertionsort/1,insertionsort'1/1,'cklt#/1,'compare#/2,'less#/2,append#/2,append'1#/2,flatten#/1 ,flatten'1#/1,flattensort#/1,insert#/2,insert'1#/2,insert'2#/4,insertionsort#/1,insertionsort'1#/1} / {'0/0 ,'EQ/0,'GT/0,'LT/0,'false/0,'neg/1,'pos/1,'s/1,'true/0,dd/2,leaf/0,nil/0,node/3,c_1/0,c_2/0,c_3/0,c_4/0 ,c_5/0,c_6/0,c_7/0,c_8/0,c_9/1,c_10/0,c_11/0,c_12/0,c_13/1,c_14/0,c_15/1,c_16/1,c_17/1,c_18/1,c_19/0,c_20/1 ,c_21/0,c_22/4,c_23/2,c_24/1,c_25/2,c_26/0,c_27/0,c_28/1,c_29/1,c_30/2,c_31/0} - Obligation: innermost runtime complexity wrt. defined symbols {'cklt#,'compare#,'less#,append#,append'1#,flatten# ,flatten'1#,flattensort#,insert#,insert'1#,insert'2#,insertionsort#,insertionsort'1#} and constructors {'0 ,'EQ,'GT,'LT,'false,'neg,'pos,'s,'true,dd,leaf,nil,node} + Applied Processor: RemoveHeads + Details: Consider the dependency graph 1:S:append#(l1,l2) -> c_17(append'1#(l1,l2)) -->_1 append'1#(dd(x,xs),l2) -> c_18(append#(xs,l2)):2 2:S:append'1#(dd(x,xs),l2) -> c_18(append#(xs,l2)) -->_1 append#(l1,l2) -> c_17(append'1#(l1,l2)):1 3:S:insert#(x,l) -> c_24(insert'1#(l,x)) -->_1 insert'1#(dd(y,ys),x) -> c_25(insert'2#('less(y,x),x,y,ys),'less#(y,x)):4 4:S:insert'1#(dd(y,ys),x) -> c_25(insert'2#('less(y,x),x,y,ys),'less#(y,x)) -->_1 insert'2#('true(),x,y,ys) -> c_28(insert#(x,ys)):5 5:S:insert'2#('true(),x,y,ys) -> c_28(insert#(x,ys)) -->_1 insert#(x,l) -> c_24(insert'1#(l,x)):3 6:W:flatten#(t) -> flatten'1#(t) -->_1 flatten'1#(node(l,t1,t2)) -> flatten#(t2):10 -->_1 flatten'1#(node(l,t1,t2)) -> flatten#(t1):9 -->_1 flatten'1#(node(l,t1,t2)) -> append#(flatten(t1),flatten(t2)):8 -->_1 flatten'1#(node(l,t1,t2)) -> append#(l,append(flatten(t1),flatten(t2))):7 7:W:flatten'1#(node(l,t1,t2)) -> append#(l,append(flatten(t1),flatten(t2))) -->_1 append#(l1,l2) -> c_17(append'1#(l1,l2)):1 8:W:flatten'1#(node(l,t1,t2)) -> append#(flatten(t1),flatten(t2)) -->_1 append#(l1,l2) -> c_17(append'1#(l1,l2)):1 9:W:flatten'1#(node(l,t1,t2)) -> flatten#(t1) -->_1 flatten#(t) -> flatten'1#(t):6 10:W:flatten'1#(node(l,t1,t2)) -> flatten#(t2) -->_1 flatten#(t) -> flatten'1#(t):6 11:W:flattensort#(t) -> flatten#(t) -->_1 flatten#(t) -> flatten'1#(t):6 12:W:flattensort#(t) -> insertionsort#(flatten(t)) -->_1 insertionsort#(l) -> insertionsort'1#(l):13 13:W:insertionsort#(l) -> insertionsort'1#(l) -->_1 insertionsort'1#(dd(x,xs)) -> insertionsort#(xs):15 -->_1 insertionsort'1#(dd(x,xs)) -> insert#(x,insertionsort(xs)):14 14:W:insertionsort'1#(dd(x,xs)) -> insert#(x,insertionsort(xs)) -->_1 insert#(x,l) -> c_24(insert'1#(l,x)):3 15:W:insertionsort'1#(dd(x,xs)) -> insertionsort#(xs) -->_1 insertionsort#(l) -> insertionsort'1#(l):13 Following roots of the dependency graph are removed, as the considered set of starting terms is closed under reduction with respect to these rules (modulo compound contexts). [(11,flattensort#(t) -> flatten#(t))] *** Step 6.b:1.a:2: SimplifyRHS WORST_CASE(?,O(n^1)) + Considered Problem: - Strict DPs: append#(l1,l2) -> c_17(append'1#(l1,l2)) append'1#(dd(x,xs),l2) -> c_18(append#(xs,l2)) insert#(x,l) -> c_24(insert'1#(l,x)) insert'1#(dd(y,ys),x) -> c_25(insert'2#('less(y,x),x,y,ys),'less#(y,x)) insert'2#('true(),x,y,ys) -> c_28(insert#(x,ys)) - Weak DPs: flatten#(t) -> flatten'1#(t) flatten'1#(node(l,t1,t2)) -> append#(l,append(flatten(t1),flatten(t2))) flatten'1#(node(l,t1,t2)) -> append#(flatten(t1),flatten(t2)) flatten'1#(node(l,t1,t2)) -> flatten#(t1) flatten'1#(node(l,t1,t2)) -> flatten#(t2) flattensort#(t) -> insertionsort#(flatten(t)) insertionsort#(l) -> insertionsort'1#(l) insertionsort'1#(dd(x,xs)) -> insert#(x,insertionsort(xs)) insertionsort'1#(dd(x,xs)) -> insertionsort#(xs) - Weak TRS: 'cklt('EQ()) -> 'false() 'cklt('GT()) -> 'false() 'cklt('LT()) -> 'true() 'compare('0(),'0()) -> 'EQ() 'compare('0(),'neg(y)) -> 'GT() 'compare('0(),'pos(y)) -> 'LT() 'compare('0(),'s(y)) -> 'LT() 'compare('neg(x),'0()) -> 'LT() 'compare('neg(x),'neg(y)) -> 'compare(y,x) 'compare('neg(x),'pos(y)) -> 'LT() 'compare('pos(x),'0()) -> 'GT() 'compare('pos(x),'neg(y)) -> 'GT() 'compare('pos(x),'pos(y)) -> 'compare(x,y) 'compare('s(x),'0()) -> 'GT() 'compare('s(x),'s(y)) -> 'compare(x,y) 'less(x,y) -> 'cklt('compare(x,y)) append(l1,l2) -> append'1(l1,l2) append'1(dd(x,xs),l2) -> dd(x,append(xs,l2)) append'1(nil(),l2) -> l2 flatten(t) -> flatten'1(t) flatten'1(leaf()) -> nil() flatten'1(node(l,t1,t2)) -> append(l,append(flatten(t1),flatten(t2))) insert(x,l) -> insert'1(l,x) insert'1(dd(y,ys),x) -> insert'2('less(y,x),x,y,ys) insert'1(nil(),x) -> dd(x,nil()) insert'2('false(),x,y,ys) -> dd(x,dd(y,ys)) insert'2('true(),x,y,ys) -> dd(y,insert(x,ys)) insertionsort(l) -> insertionsort'1(l) insertionsort'1(dd(x,xs)) -> insert(x,insertionsort(xs)) insertionsort'1(nil()) -> nil() - Signature: {'cklt/1,'compare/2,'less/2,append/2,append'1/2,flatten/1,flatten'1/1,flattensort/1,insert/2,insert'1/2 ,insert'2/4,insertionsort/1,insertionsort'1/1,'cklt#/1,'compare#/2,'less#/2,append#/2,append'1#/2,flatten#/1 ,flatten'1#/1,flattensort#/1,insert#/2,insert'1#/2,insert'2#/4,insertionsort#/1,insertionsort'1#/1} / {'0/0 ,'EQ/0,'GT/0,'LT/0,'false/0,'neg/1,'pos/1,'s/1,'true/0,dd/2,leaf/0,nil/0,node/3,c_1/0,c_2/0,c_3/0,c_4/0 ,c_5/0,c_6/0,c_7/0,c_8/0,c_9/1,c_10/0,c_11/0,c_12/0,c_13/1,c_14/0,c_15/1,c_16/1,c_17/1,c_18/1,c_19/0,c_20/1 ,c_21/0,c_22/4,c_23/2,c_24/1,c_25/2,c_26/0,c_27/0,c_28/1,c_29/1,c_30/2,c_31/0} - Obligation: innermost runtime complexity wrt. defined symbols {'cklt#,'compare#,'less#,append#,append'1#,flatten# ,flatten'1#,flattensort#,insert#,insert'1#,insert'2#,insertionsort#,insertionsort'1#} and constructors {'0 ,'EQ,'GT,'LT,'false,'neg,'pos,'s,'true,dd,leaf,nil,node} + Applied Processor: SimplifyRHS + Details: Consider the dependency graph 1:S:append#(l1,l2) -> c_17(append'1#(l1,l2)) -->_1 append'1#(dd(x,xs),l2) -> c_18(append#(xs,l2)):2 2:S:append'1#(dd(x,xs),l2) -> c_18(append#(xs,l2)) -->_1 append#(l1,l2) -> c_17(append'1#(l1,l2)):1 3:S:insert#(x,l) -> c_24(insert'1#(l,x)) -->_1 insert'1#(dd(y,ys),x) -> c_25(insert'2#('less(y,x),x,y,ys),'less#(y,x)):4 4:S:insert'1#(dd(y,ys),x) -> c_25(insert'2#('less(y,x),x,y,ys),'less#(y,x)) -->_1 insert'2#('true(),x,y,ys) -> c_28(insert#(x,ys)):5 5:S:insert'2#('true(),x,y,ys) -> c_28(insert#(x,ys)) -->_1 insert#(x,l) -> c_24(insert'1#(l,x)):3 6:W:flatten#(t) -> flatten'1#(t) -->_1 flatten'1#(node(l,t1,t2)) -> flatten#(t2):10 -->_1 flatten'1#(node(l,t1,t2)) -> flatten#(t1):9 -->_1 flatten'1#(node(l,t1,t2)) -> append#(flatten(t1),flatten(t2)):8 -->_1 flatten'1#(node(l,t1,t2)) -> append#(l,append(flatten(t1),flatten(t2))):7 7:W:flatten'1#(node(l,t1,t2)) -> append#(l,append(flatten(t1),flatten(t2))) -->_1 append#(l1,l2) -> c_17(append'1#(l1,l2)):1 8:W:flatten'1#(node(l,t1,t2)) -> append#(flatten(t1),flatten(t2)) -->_1 append#(l1,l2) -> c_17(append'1#(l1,l2)):1 9:W:flatten'1#(node(l,t1,t2)) -> flatten#(t1) -->_1 flatten#(t) -> flatten'1#(t):6 10:W:flatten'1#(node(l,t1,t2)) -> flatten#(t2) -->_1 flatten#(t) -> flatten'1#(t):6 12:W:flattensort#(t) -> insertionsort#(flatten(t)) -->_1 insertionsort#(l) -> insertionsort'1#(l):13 13:W:insertionsort#(l) -> insertionsort'1#(l) -->_1 insertionsort'1#(dd(x,xs)) -> insertionsort#(xs):15 -->_1 insertionsort'1#(dd(x,xs)) -> insert#(x,insertionsort(xs)):14 14:W:insertionsort'1#(dd(x,xs)) -> insert#(x,insertionsort(xs)) -->_1 insert#(x,l) -> c_24(insert'1#(l,x)):3 15:W:insertionsort'1#(dd(x,xs)) -> insertionsort#(xs) -->_1 insertionsort#(l) -> insertionsort'1#(l):13 Due to missing edges in the depndency graph, the right-hand sides of following rules could be simplified: insert'1#(dd(y,ys),x) -> c_25(insert'2#('less(y,x),x,y,ys)) *** Step 6.b:1.a:3: Ara WORST_CASE(?,O(n^1)) + Considered Problem: - Strict DPs: append#(l1,l2) -> c_17(append'1#(l1,l2)) append'1#(dd(x,xs),l2) -> c_18(append#(xs,l2)) insert#(x,l) -> c_24(insert'1#(l,x)) insert'1#(dd(y,ys),x) -> c_25(insert'2#('less(y,x),x,y,ys)) insert'2#('true(),x,y,ys) -> c_28(insert#(x,ys)) - Weak DPs: flatten#(t) -> flatten'1#(t) flatten'1#(node(l,t1,t2)) -> append#(l,append(flatten(t1),flatten(t2))) flatten'1#(node(l,t1,t2)) -> append#(flatten(t1),flatten(t2)) flatten'1#(node(l,t1,t2)) -> flatten#(t1) flatten'1#(node(l,t1,t2)) -> flatten#(t2) flattensort#(t) -> insertionsort#(flatten(t)) insertionsort#(l) -> insertionsort'1#(l) insertionsort'1#(dd(x,xs)) -> insert#(x,insertionsort(xs)) insertionsort'1#(dd(x,xs)) -> insertionsort#(xs) - Weak TRS: 'cklt('EQ()) -> 'false() 'cklt('GT()) -> 'false() 'cklt('LT()) -> 'true() 'compare('0(),'0()) -> 'EQ() 'compare('0(),'neg(y)) -> 'GT() 'compare('0(),'pos(y)) -> 'LT() 'compare('0(),'s(y)) -> 'LT() 'compare('neg(x),'0()) -> 'LT() 'compare('neg(x),'neg(y)) -> 'compare(y,x) 'compare('neg(x),'pos(y)) -> 'LT() 'compare('pos(x),'0()) -> 'GT() 'compare('pos(x),'neg(y)) -> 'GT() 'compare('pos(x),'pos(y)) -> 'compare(x,y) 'compare('s(x),'0()) -> 'GT() 'compare('s(x),'s(y)) -> 'compare(x,y) 'less(x,y) -> 'cklt('compare(x,y)) append(l1,l2) -> append'1(l1,l2) append'1(dd(x,xs),l2) -> dd(x,append(xs,l2)) append'1(nil(),l2) -> l2 flatten(t) -> flatten'1(t) flatten'1(leaf()) -> nil() flatten'1(node(l,t1,t2)) -> append(l,append(flatten(t1),flatten(t2))) insert(x,l) -> insert'1(l,x) insert'1(dd(y,ys),x) -> insert'2('less(y,x),x,y,ys) insert'1(nil(),x) -> dd(x,nil()) insert'2('false(),x,y,ys) -> dd(x,dd(y,ys)) insert'2('true(),x,y,ys) -> dd(y,insert(x,ys)) insertionsort(l) -> insertionsort'1(l) insertionsort'1(dd(x,xs)) -> insert(x,insertionsort(xs)) insertionsort'1(nil()) -> nil() - Signature: {'cklt/1,'compare/2,'less/2,append/2,append'1/2,flatten/1,flatten'1/1,flattensort/1,insert/2,insert'1/2 ,insert'2/4,insertionsort/1,insertionsort'1/1,'cklt#/1,'compare#/2,'less#/2,append#/2,append'1#/2,flatten#/1 ,flatten'1#/1,flattensort#/1,insert#/2,insert'1#/2,insert'2#/4,insertionsort#/1,insertionsort'1#/1} / {'0/0 ,'EQ/0,'GT/0,'LT/0,'false/0,'neg/1,'pos/1,'s/1,'true/0,dd/2,leaf/0,nil/0,node/3,c_1/0,c_2/0,c_3/0,c_4/0 ,c_5/0,c_6/0,c_7/0,c_8/0,c_9/1,c_10/0,c_11/0,c_12/0,c_13/1,c_14/0,c_15/1,c_16/1,c_17/1,c_18/1,c_19/0,c_20/1 ,c_21/0,c_22/4,c_23/2,c_24/1,c_25/1,c_26/0,c_27/0,c_28/1,c_29/1,c_30/2,c_31/0} - Obligation: innermost runtime complexity wrt. defined symbols {'cklt#,'compare#,'less#,append#,append'1#,flatten# ,flatten'1#,flattensort#,insert#,insert'1#,insert'2#,insertionsort#,insertionsort'1#} and constructors {'0 ,'EQ,'GT,'LT,'false,'neg,'pos,'s,'true,dd,leaf,nil,node} + Applied Processor: Ara {araHeuristics = NoHeuristics, minDegree = 1, maxDegree = 2, araTimeout = 8, araRuleShifting = Just 1} + Details: Signatures used: ---------------- '0 :: [] -(0)-> "A"(0) 'EQ :: [] -(0)-> "A"(0) 'EQ :: [] -(0)-> "A"(15) 'GT :: [] -(0)-> "A"(0) 'GT :: [] -(0)-> "A"(15) 'LT :: [] -(0)-> "A"(0) 'LT :: [] -(0)-> "A"(15) 'cklt :: ["A"(0)] -(0)-> "A"(9) 'compare :: ["A"(0) x "A"(0)] -(0)-> "A"(9) 'false :: [] -(0)-> "A"(0) 'false :: [] -(0)-> "A"(15) 'less :: ["A"(0) x "A"(0)] -(0)-> "A"(9) 'neg :: ["A"(0)] -(0)-> "A"(0) 'pos :: ["A"(0)] -(0)-> "A"(0) 's :: ["A"(0)] -(0)-> "A"(0) 'true :: [] -(0)-> "A"(0) 'true :: [] -(0)-> "A"(15) append :: ["A"(15) x "A"(15)] -(0)-> "A"(15) append'1 :: ["A"(15) x "A"(15)] -(0)-> "A"(15) dd :: ["A"(15) x "A"(15)] -(15)-> "A"(15) dd :: ["A"(0) x "A"(0)] -(0)-> "A"(0) dd :: ["A"(13) x "A"(13)] -(13)-> "A"(13) dd :: ["A"(5) x "A"(5)] -(5)-> "A"(5) flatten :: ["A"(15)] -(0)-> "A"(15) flatten'1 :: ["A"(15)] -(0)-> "A"(15) insert :: ["A"(13) x "A"(0)] -(8)-> "A"(0) insert'1 :: ["A"(0) x "A"(13)] -(8)-> "A"(0) insert'2 :: ["A"(0) x "A"(13) x "A"(0) x "A"(0)] -(8)-> "A"(0) insertionsort :: ["A"(13)] -(4)-> "A"(0) insertionsort'1 :: ["A"(13)] -(1)-> "A"(0) leaf :: [] -(0)-> "A"(15) nil :: [] -(0)-> "A"(15) nil :: [] -(0)-> "A"(0) nil :: [] -(0)-> "A"(13) nil :: [] -(0)-> "A"(7) node :: ["A"(15) x "A"(15) x "A"(15)] -(15)-> "A"(15) append# :: ["A"(15) x "A"(9)] -(12)-> "A"(1) append'1# :: ["A"(15) x "A"(9)] -(9)-> "A"(1) flatten# :: ["A"(15)] -(9)-> "A"(1) flatten'1# :: ["A"(15)] -(9)-> "A"(1) flattensort# :: ["A"(15)] -(15)-> "A"(0) insert# :: ["A"(9) x "A"(0)] -(8)-> "A"(0) insert'1# :: ["A"(0) x "A"(9)] -(8)-> "A"(9) insert'2# :: ["A"(0) x "A"(9) x "A"(0) x "A"(0)] -(8)-> "A"(13) insertionsort# :: ["A"(13)] -(1)-> "A"(0) insertionsort'1# :: ["A"(13)] -(1)-> "A"(0) c_17 :: ["A"(0)] -(0)-> "A"(12) c_18 :: ["A"(1)] -(1)-> "A"(1) c_24 :: ["A"(0)] -(0)-> "A"(12) c_25 :: ["A"(11)] -(0)-> "A"(11) c_28 :: ["A"(0)] -(0)-> "A"(15) Cost-free Signatures used: -------------------------- Base Constructor Signatures used: --------------------------------- "'0_A" :: [] -(0)-> "A"(1) "'EQ_A" :: [] -(0)-> "A"(1) "'GT_A" :: [] -(0)-> "A"(1) "'LT_A" :: [] -(0)-> "A"(1) "'false_A" :: [] -(0)-> "A"(1) "'neg_A" :: ["A"(1)] -(0)-> "A"(1) "'pos_A" :: ["A"(1)] -(0)-> "A"(1) "'s_A" :: ["A"(1)] -(0)-> "A"(1) "'true_A" :: [] -(0)-> "A"(1) "c_17_A" :: ["A"(0)] -(0)-> "A"(1) "c_18_A" :: ["A"(0)] -(1)-> "A"(1) "c_24_A" :: ["A"(0)] -(0)-> "A"(1) "c_25_A" :: ["A"(0)] -(0)-> "A"(1) "c_28_A" :: ["A"(0)] -(0)-> "A"(1) "dd_A" :: ["A"(1) x "A"(1)] -(1)-> "A"(1) "leaf_A" :: [] -(0)-> "A"(1) "nil_A" :: [] -(0)-> "A"(1) "node_A" :: ["A"(1) x "A"(1) x "A"(1)] -(1)-> "A"(1) Following Still Strict Rules were Typed as: ------------------------------------------- 1. Strict: append'1#(dd(x,xs),l2) -> c_18(append#(xs,l2)) 2. Weak: append#(l1,l2) -> c_17(append'1#(l1,l2)) insert#(x,l) -> c_24(insert'1#(l,x)) insert'1#(dd(y,ys),x) -> c_25(insert'2#('less(y,x),x,y,ys)) insert'2#('true(),x,y,ys) -> c_28(insert#(x,ys)) *** Step 6.b:1.a:4: Ara WORST_CASE(?,O(n^1)) + Considered Problem: - Strict DPs: append#(l1,l2) -> c_17(append'1#(l1,l2)) insert#(x,l) -> c_24(insert'1#(l,x)) insert'1#(dd(y,ys),x) -> c_25(insert'2#('less(y,x),x,y,ys)) insert'2#('true(),x,y,ys) -> c_28(insert#(x,ys)) - Weak DPs: append'1#(dd(x,xs),l2) -> c_18(append#(xs,l2)) flatten#(t) -> flatten'1#(t) flatten'1#(node(l,t1,t2)) -> append#(l,append(flatten(t1),flatten(t2))) flatten'1#(node(l,t1,t2)) -> append#(flatten(t1),flatten(t2)) flatten'1#(node(l,t1,t2)) -> flatten#(t1) flatten'1#(node(l,t1,t2)) -> flatten#(t2) flattensort#(t) -> insertionsort#(flatten(t)) insertionsort#(l) -> insertionsort'1#(l) insertionsort'1#(dd(x,xs)) -> insert#(x,insertionsort(xs)) insertionsort'1#(dd(x,xs)) -> insertionsort#(xs) - Weak TRS: 'cklt('EQ()) -> 'false() 'cklt('GT()) -> 'false() 'cklt('LT()) -> 'true() 'compare('0(),'0()) -> 'EQ() 'compare('0(),'neg(y)) -> 'GT() 'compare('0(),'pos(y)) -> 'LT() 'compare('0(),'s(y)) -> 'LT() 'compare('neg(x),'0()) -> 'LT() 'compare('neg(x),'neg(y)) -> 'compare(y,x) 'compare('neg(x),'pos(y)) -> 'LT() 'compare('pos(x),'0()) -> 'GT() 'compare('pos(x),'neg(y)) -> 'GT() 'compare('pos(x),'pos(y)) -> 'compare(x,y) 'compare('s(x),'0()) -> 'GT() 'compare('s(x),'s(y)) -> 'compare(x,y) 'less(x,y) -> 'cklt('compare(x,y)) append(l1,l2) -> append'1(l1,l2) append'1(dd(x,xs),l2) -> dd(x,append(xs,l2)) append'1(nil(),l2) -> l2 flatten(t) -> flatten'1(t) flatten'1(leaf()) -> nil() flatten'1(node(l,t1,t2)) -> append(l,append(flatten(t1),flatten(t2))) insert(x,l) -> insert'1(l,x) insert'1(dd(y,ys),x) -> insert'2('less(y,x),x,y,ys) insert'1(nil(),x) -> dd(x,nil()) insert'2('false(),x,y,ys) -> dd(x,dd(y,ys)) insert'2('true(),x,y,ys) -> dd(y,insert(x,ys)) insertionsort(l) -> insertionsort'1(l) insertionsort'1(dd(x,xs)) -> insert(x,insertionsort(xs)) insertionsort'1(nil()) -> nil() - Signature: {'cklt/1,'compare/2,'less/2,append/2,append'1/2,flatten/1,flatten'1/1,flattensort/1,insert/2,insert'1/2 ,insert'2/4,insertionsort/1,insertionsort'1/1,'cklt#/1,'compare#/2,'less#/2,append#/2,append'1#/2,flatten#/1 ,flatten'1#/1,flattensort#/1,insert#/2,insert'1#/2,insert'2#/4,insertionsort#/1,insertionsort'1#/1} / {'0/0 ,'EQ/0,'GT/0,'LT/0,'false/0,'neg/1,'pos/1,'s/1,'true/0,dd/2,leaf/0,nil/0,node/3,c_1/0,c_2/0,c_3/0,c_4/0 ,c_5/0,c_6/0,c_7/0,c_8/0,c_9/1,c_10/0,c_11/0,c_12/0,c_13/1,c_14/0,c_15/1,c_16/1,c_17/1,c_18/1,c_19/0,c_20/1 ,c_21/0,c_22/4,c_23/2,c_24/1,c_25/1,c_26/0,c_27/0,c_28/1,c_29/1,c_30/2,c_31/0} - Obligation: innermost runtime complexity wrt. defined symbols {'cklt#,'compare#,'less#,append#,append'1#,flatten# ,flatten'1#,flattensort#,insert#,insert'1#,insert'2#,insertionsort#,insertionsort'1#} and constructors {'0 ,'EQ,'GT,'LT,'false,'neg,'pos,'s,'true,dd,leaf,nil,node} + Applied Processor: Ara {araHeuristics = NoHeuristics, minDegree = 1, maxDegree = 2, araTimeout = 8, araRuleShifting = Just 1} + Details: Signatures used: ---------------- '0 :: [] -(0)-> "A"(0) 'EQ :: [] -(0)-> "A"(0) 'EQ :: [] -(0)-> "A"(15) 'GT :: [] -(0)-> "A"(0) 'GT :: [] -(0)-> "A"(15) 'LT :: [] -(0)-> "A"(0) 'LT :: [] -(0)-> "A"(15) 'cklt :: ["A"(0)] -(0)-> "A"(9) 'compare :: ["A"(0) x "A"(0)] -(0)-> "A"(9) 'false :: [] -(0)-> "A"(0) 'false :: [] -(0)-> "A"(15) 'less :: ["A"(0) x "A"(0)] -(0)-> "A"(9) 'neg :: ["A"(0)] -(0)-> "A"(0) 'pos :: ["A"(0)] -(0)-> "A"(0) 's :: ["A"(0)] -(0)-> "A"(0) 'true :: [] -(0)-> "A"(0) 'true :: [] -(0)-> "A"(15) append :: ["A"(13) x "A"(13)] -(1)-> "A"(13) append'1 :: ["A"(13) x "A"(13)] -(1)-> "A"(13) dd :: ["A"(7) x "A"(7)] -(7)-> "A"(7) dd :: ["A"(13) x "A"(13)] -(13)-> "A"(13) dd :: ["A"(9) x "A"(9)] -(9)-> "A"(9) dd :: ["A"(10) x "A"(10)] -(10)-> "A"(10) dd :: ["A"(8) x "A"(8)] -(8)-> "A"(8) flatten :: ["A"(15)] -(1)-> "A"(13) flatten'1 :: ["A"(15)] -(1)-> "A"(13) insert :: ["A"(8) x "A"(7)] -(8)-> "A"(7) insert'1 :: ["A"(7) x "A"(8)] -(8)-> "A"(7) insert'2 :: ["A"(0) x "A"(8) x "A"(7) x "A"(7)] -(15)-> "A"(7) insertionsort :: ["A"(9)] -(2)-> "A"(7) insertionsort'1 :: ["A"(9)] -(1)-> "A"(7) leaf :: [] -(0)-> "A"(15) nil :: [] -(0)-> "A"(13) nil :: [] -(0)-> "A"(7) nil :: [] -(0)-> "A"(9) nil :: [] -(0)-> "A"(15) node :: ["A"(15) x "A"(15) x "A"(15)] -(15)-> "A"(15) append# :: ["A"(13) x "A"(9)] -(9)-> "A"(1) append'1# :: ["A"(13) x "A"(9)] -(5)-> "A"(12) flatten# :: ["A"(15)] -(9)-> "A"(1) flatten'1# :: ["A"(15)] -(9)-> "A"(1) flattensort# :: ["A"(15)] -(14)-> "A"(0) insert# :: ["A"(8) x "A"(7)] -(8)-> "A"(0) insert'1# :: ["A"(7) x "A"(8)] -(8)-> "A"(13) insert'2# :: ["A"(0) x "A"(8) x "A"(1) x "A"(7)] -(9)-> "A"(15) insertionsort# :: ["A"(10)] -(9)-> "A"(0) insertionsort'1# :: ["A"(10)] -(5)-> "A"(0) c_17 :: ["A"(0)] -(0)-> "A"(12) c_18 :: ["A"(0)] -(0)-> "A"(15) c_24 :: ["A"(9)] -(0)-> "A"(9) c_25 :: ["A"(15)] -(0)-> "A"(15) c_28 :: ["A"(0)] -(0)-> "A"(15) Cost-free Signatures used: -------------------------- Base Constructor Signatures used: --------------------------------- "'0_A" :: [] -(0)-> "A"(1) "'EQ_A" :: [] -(0)-> "A"(1) "'GT_A" :: [] -(0)-> "A"(1) "'LT_A" :: [] -(0)-> "A"(1) "'false_A" :: [] -(0)-> "A"(1) "'neg_A" :: ["A"(1)] -(1)-> "A"(1) "'pos_A" :: ["A"(1)] -(1)-> "A"(1) "'s_A" :: ["A"(1)] -(1)-> "A"(1) "'true_A" :: [] -(0)-> "A"(1) "c_17_A" :: ["A"(0)] -(0)-> "A"(1) "c_18_A" :: ["A"(0)] -(0)-> "A"(1) "c_24_A" :: ["A"(0)] -(0)-> "A"(1) "c_25_A" :: ["A"(0)] -(0)-> "A"(1) "c_28_A" :: ["A"(0)] -(0)-> "A"(1) "dd_A" :: ["A"(1) x "A"(1)] -(1)-> "A"(1) "leaf_A" :: [] -(0)-> "A"(1) "nil_A" :: [] -(0)-> "A"(1) "node_A" :: ["A"(1) x "A"(1) x "A"(1)] -(1)-> "A"(1) Following Still Strict Rules were Typed as: ------------------------------------------- 1. Strict: append#(l1,l2) -> c_17(append'1#(l1,l2)) insert'2#('true(),x,y,ys) -> c_28(insert#(x,ys)) 2. Weak: insert#(x,l) -> c_24(insert'1#(l,x)) insert'1#(dd(y,ys),x) -> c_25(insert'2#('less(y,x),x,y,ys)) *** Step 6.b:1.a:5: Ara WORST_CASE(?,O(n^1)) + Considered Problem: - Strict DPs: insert#(x,l) -> c_24(insert'1#(l,x)) insert'1#(dd(y,ys),x) -> c_25(insert'2#('less(y,x),x,y,ys)) - Weak DPs: append#(l1,l2) -> c_17(append'1#(l1,l2)) append'1#(dd(x,xs),l2) -> c_18(append#(xs,l2)) flatten#(t) -> flatten'1#(t) flatten'1#(node(l,t1,t2)) -> append#(l,append(flatten(t1),flatten(t2))) flatten'1#(node(l,t1,t2)) -> append#(flatten(t1),flatten(t2)) flatten'1#(node(l,t1,t2)) -> flatten#(t1) flatten'1#(node(l,t1,t2)) -> flatten#(t2) flattensort#(t) -> insertionsort#(flatten(t)) insert'2#('true(),x,y,ys) -> c_28(insert#(x,ys)) insertionsort#(l) -> insertionsort'1#(l) insertionsort'1#(dd(x,xs)) -> insert#(x,insertionsort(xs)) insertionsort'1#(dd(x,xs)) -> insertionsort#(xs) - Weak TRS: 'cklt('EQ()) -> 'false() 'cklt('GT()) -> 'false() 'cklt('LT()) -> 'true() 'compare('0(),'0()) -> 'EQ() 'compare('0(),'neg(y)) -> 'GT() 'compare('0(),'pos(y)) -> 'LT() 'compare('0(),'s(y)) -> 'LT() 'compare('neg(x),'0()) -> 'LT() 'compare('neg(x),'neg(y)) -> 'compare(y,x) 'compare('neg(x),'pos(y)) -> 'LT() 'compare('pos(x),'0()) -> 'GT() 'compare('pos(x),'neg(y)) -> 'GT() 'compare('pos(x),'pos(y)) -> 'compare(x,y) 'compare('s(x),'0()) -> 'GT() 'compare('s(x),'s(y)) -> 'compare(x,y) 'less(x,y) -> 'cklt('compare(x,y)) append(l1,l2) -> append'1(l1,l2) append'1(dd(x,xs),l2) -> dd(x,append(xs,l2)) append'1(nil(),l2) -> l2 flatten(t) -> flatten'1(t) flatten'1(leaf()) -> nil() flatten'1(node(l,t1,t2)) -> append(l,append(flatten(t1),flatten(t2))) insert(x,l) -> insert'1(l,x) insert'1(dd(y,ys),x) -> insert'2('less(y,x),x,y,ys) insert'1(nil(),x) -> dd(x,nil()) insert'2('false(),x,y,ys) -> dd(x,dd(y,ys)) insert'2('true(),x,y,ys) -> dd(y,insert(x,ys)) insertionsort(l) -> insertionsort'1(l) insertionsort'1(dd(x,xs)) -> insert(x,insertionsort(xs)) insertionsort'1(nil()) -> nil() - Signature: {'cklt/1,'compare/2,'less/2,append/2,append'1/2,flatten/1,flatten'1/1,flattensort/1,insert/2,insert'1/2 ,insert'2/4,insertionsort/1,insertionsort'1/1,'cklt#/1,'compare#/2,'less#/2,append#/2,append'1#/2,flatten#/1 ,flatten'1#/1,flattensort#/1,insert#/2,insert'1#/2,insert'2#/4,insertionsort#/1,insertionsort'1#/1} / {'0/0 ,'EQ/0,'GT/0,'LT/0,'false/0,'neg/1,'pos/1,'s/1,'true/0,dd/2,leaf/0,nil/0,node/3,c_1/0,c_2/0,c_3/0,c_4/0 ,c_5/0,c_6/0,c_7/0,c_8/0,c_9/1,c_10/0,c_11/0,c_12/0,c_13/1,c_14/0,c_15/1,c_16/1,c_17/1,c_18/1,c_19/0,c_20/1 ,c_21/0,c_22/4,c_23/2,c_24/1,c_25/1,c_26/0,c_27/0,c_28/1,c_29/1,c_30/2,c_31/0} - Obligation: innermost runtime complexity wrt. defined symbols {'cklt#,'compare#,'less#,append#,append'1#,flatten# ,flatten'1#,flattensort#,insert#,insert'1#,insert'2#,insertionsort#,insertionsort'1#} and constructors {'0 ,'EQ,'GT,'LT,'false,'neg,'pos,'s,'true,dd,leaf,nil,node} + Applied Processor: Ara {araHeuristics = NoHeuristics, minDegree = 1, maxDegree = 2, araTimeout = 8, araRuleShifting = Just 1} + Details: Signatures used: ---------------- '0 :: [] -(0)-> "A"(0) 'EQ :: [] -(0)-> "A"(0) 'EQ :: [] -(0)-> "A"(15) 'GT :: [] -(0)-> "A"(0) 'GT :: [] -(0)-> "A"(15) 'LT :: [] -(0)-> "A"(0) 'LT :: [] -(0)-> "A"(15) 'cklt :: ["A"(0)] -(0)-> "A"(9) 'compare :: ["A"(0) x "A"(0)] -(0)-> "A"(9) 'false :: [] -(0)-> "A"(0) 'false :: [] -(0)-> "A"(15) 'less :: ["A"(0) x "A"(0)] -(0)-> "A"(9) 'neg :: ["A"(0)] -(0)-> "A"(0) 'pos :: ["A"(0)] -(0)-> "A"(0) 's :: ["A"(0)] -(0)-> "A"(0) 'true :: [] -(0)-> "A"(0) 'true :: [] -(0)-> "A"(15) append :: ["A"(15) x "A"(15)] -(0)-> "A"(15) append'1 :: ["A"(15) x "A"(15)] -(0)-> "A"(15) dd :: ["A"(4) x "A"(4)] -(4)-> "A"(4) dd :: ["A"(15) x "A"(15)] -(15)-> "A"(15) dd :: ["A"(13) x "A"(13)] -(13)-> "A"(13) flatten :: ["A"(15)] -(0)-> "A"(15) flatten'1 :: ["A"(15)] -(0)-> "A"(15) insert :: ["A"(14) x "A"(4)] -(8)-> "A"(4) insert'1 :: ["A"(4) x "A"(14)] -(8)-> "A"(4) insert'2 :: ["A"(0) x "A"(14) x "A"(4) x "A"(4)] -(12)-> "A"(4) insertionsort :: ["A"(15)] -(1)-> "A"(4) insertionsort'1 :: ["A"(15)] -(1)-> "A"(4) leaf :: [] -(0)-> "A"(15) nil :: [] -(0)-> "A"(15) nil :: [] -(0)-> "A"(4) nil :: [] -(0)-> "A"(11) node :: ["A"(15) x "A"(15) x "A"(15)] -(0)-> "A"(15) append# :: ["A"(13) x "A"(9)] -(3)-> "A"(1) append'1# :: ["A"(13) x "A"(9)] -(1)-> "A"(1) flatten# :: ["A"(15)] -(14)-> "A"(1) flatten'1# :: ["A"(15)] -(14)-> "A"(1) flattensort# :: ["A"(15)] -(15)-> "A"(0) insert# :: ["A"(12) x "A"(4)] -(14)-> "A"(0) insert'1# :: ["A"(4) x "A"(12)] -(12)-> "A"(9) insert'2# :: ["A"(0) x "A"(12) x "A"(1) x "A"(4)] -(14)-> "A"(13) insertionsort# :: ["A"(15)] -(1)-> "A"(0) insertionsort'1# :: ["A"(15)] -(1)-> "A"(0) c_17 :: ["A"(1)] -(1)-> "A"(1) c_18 :: ["A"(0)] -(0)-> "A"(7) c_24 :: ["A"(1)] -(1)-> "A"(1) c_25 :: ["A"(0)] -(0)-> "A"(15) c_28 :: ["A"(0)] -(0)-> "A"(15) Cost-free Signatures used: -------------------------- Base Constructor Signatures used: --------------------------------- "'0_A" :: [] -(0)-> "A"(1) "'EQ_A" :: [] -(0)-> "A"(1) "'GT_A" :: [] -(0)-> "A"(1) "'LT_A" :: [] -(0)-> "A"(1) "'false_A" :: [] -(0)-> "A"(1) "'neg_A" :: ["A"(1)] -(1)-> "A"(1) "'pos_A" :: ["A"(1)] -(1)-> "A"(1) "'s_A" :: ["A"(1)] -(1)-> "A"(1) "'true_A" :: [] -(0)-> "A"(1) "c_17_A" :: ["A"(0)] -(1)-> "A"(1) "c_18_A" :: ["A"(0)] -(0)-> "A"(1) "c_24_A" :: ["A"(0)] -(1)-> "A"(1) "c_25_A" :: ["A"(0)] -(0)-> "A"(1) "c_28_A" :: ["A"(0)] -(0)-> "A"(1) "dd_A" :: ["A"(1) x "A"(1)] -(1)-> "A"(1) "leaf_A" :: [] -(0)-> "A"(1) "nil_A" :: [] -(0)-> "A"(1) "node_A" :: ["A"(1) x "A"(1) x "A"(1)] -(0)-> "A"(1) Following Still Strict Rules were Typed as: ------------------------------------------- 1. Strict: insert'1#(dd(y,ys),x) -> c_25(insert'2#('less(y,x),x,y,ys)) 2. Weak: insert#(x,l) -> c_24(insert'1#(l,x)) *** Step 6.b:1.a:6: Ara WORST_CASE(?,O(n^1)) + Considered Problem: - Strict DPs: insert#(x,l) -> c_24(insert'1#(l,x)) - Weak DPs: append#(l1,l2) -> c_17(append'1#(l1,l2)) append'1#(dd(x,xs),l2) -> c_18(append#(xs,l2)) flatten#(t) -> flatten'1#(t) flatten'1#(node(l,t1,t2)) -> append#(l,append(flatten(t1),flatten(t2))) flatten'1#(node(l,t1,t2)) -> append#(flatten(t1),flatten(t2)) flatten'1#(node(l,t1,t2)) -> flatten#(t1) flatten'1#(node(l,t1,t2)) -> flatten#(t2) flattensort#(t) -> insertionsort#(flatten(t)) insert'1#(dd(y,ys),x) -> c_25(insert'2#('less(y,x),x,y,ys)) insert'2#('true(),x,y,ys) -> c_28(insert#(x,ys)) insertionsort#(l) -> insertionsort'1#(l) insertionsort'1#(dd(x,xs)) -> insert#(x,insertionsort(xs)) insertionsort'1#(dd(x,xs)) -> insertionsort#(xs) - Weak TRS: 'cklt('EQ()) -> 'false() 'cklt('GT()) -> 'false() 'cklt('LT()) -> 'true() 'compare('0(),'0()) -> 'EQ() 'compare('0(),'neg(y)) -> 'GT() 'compare('0(),'pos(y)) -> 'LT() 'compare('0(),'s(y)) -> 'LT() 'compare('neg(x),'0()) -> 'LT() 'compare('neg(x),'neg(y)) -> 'compare(y,x) 'compare('neg(x),'pos(y)) -> 'LT() 'compare('pos(x),'0()) -> 'GT() 'compare('pos(x),'neg(y)) -> 'GT() 'compare('pos(x),'pos(y)) -> 'compare(x,y) 'compare('s(x),'0()) -> 'GT() 'compare('s(x),'s(y)) -> 'compare(x,y) 'less(x,y) -> 'cklt('compare(x,y)) append(l1,l2) -> append'1(l1,l2) append'1(dd(x,xs),l2) -> dd(x,append(xs,l2)) append'1(nil(),l2) -> l2 flatten(t) -> flatten'1(t) flatten'1(leaf()) -> nil() flatten'1(node(l,t1,t2)) -> append(l,append(flatten(t1),flatten(t2))) insert(x,l) -> insert'1(l,x) insert'1(dd(y,ys),x) -> insert'2('less(y,x),x,y,ys) insert'1(nil(),x) -> dd(x,nil()) insert'2('false(),x,y,ys) -> dd(x,dd(y,ys)) insert'2('true(),x,y,ys) -> dd(y,insert(x,ys)) insertionsort(l) -> insertionsort'1(l) insertionsort'1(dd(x,xs)) -> insert(x,insertionsort(xs)) insertionsort'1(nil()) -> nil() - Signature: {'cklt/1,'compare/2,'less/2,append/2,append'1/2,flatten/1,flatten'1/1,flattensort/1,insert/2,insert'1/2 ,insert'2/4,insertionsort/1,insertionsort'1/1,'cklt#/1,'compare#/2,'less#/2,append#/2,append'1#/2,flatten#/1 ,flatten'1#/1,flattensort#/1,insert#/2,insert'1#/2,insert'2#/4,insertionsort#/1,insertionsort'1#/1} / {'0/0 ,'EQ/0,'GT/0,'LT/0,'false/0,'neg/1,'pos/1,'s/1,'true/0,dd/2,leaf/0,nil/0,node/3,c_1/0,c_2/0,c_3/0,c_4/0 ,c_5/0,c_6/0,c_7/0,c_8/0,c_9/1,c_10/0,c_11/0,c_12/0,c_13/1,c_14/0,c_15/1,c_16/1,c_17/1,c_18/1,c_19/0,c_20/1 ,c_21/0,c_22/4,c_23/2,c_24/1,c_25/1,c_26/0,c_27/0,c_28/1,c_29/1,c_30/2,c_31/0} - Obligation: innermost runtime complexity wrt. defined symbols {'cklt#,'compare#,'less#,append#,append'1#,flatten# ,flatten'1#,flattensort#,insert#,insert'1#,insert'2#,insertionsort#,insertionsort'1#} and constructors {'0 ,'EQ,'GT,'LT,'false,'neg,'pos,'s,'true,dd,leaf,nil,node} + Applied Processor: Ara {araHeuristics = NoHeuristics, minDegree = 1, maxDegree = 2, araTimeout = 8, araRuleShifting = Just 1} + Details: Signatures used: ---------------- '0 :: [] -(0)-> "A"(0) 'EQ :: [] -(0)-> "A"(0) 'EQ :: [] -(0)-> "A"(15) 'GT :: [] -(0)-> "A"(0) 'GT :: [] -(0)-> "A"(15) 'LT :: [] -(0)-> "A"(0) 'LT :: [] -(0)-> "A"(15) 'cklt :: ["A"(0)] -(0)-> "A"(15) 'compare :: ["A"(0) x "A"(0)] -(0)-> "A"(9) 'false :: [] -(0)-> "A"(1) 'false :: [] -(0)-> "A"(15) 'less :: ["A"(0) x "A"(0)] -(0)-> "A"(14) 'neg :: ["A"(0)] -(0)-> "A"(0) 'pos :: ["A"(0)] -(0)-> "A"(0) 's :: ["A"(0)] -(0)-> "A"(0) 'true :: [] -(0)-> "A"(1) 'true :: [] -(0)-> "A"(15) append :: ["A"(13) x "A"(13)] -(0)-> "A"(13) append'1 :: ["A"(13) x "A"(13)] -(0)-> "A"(13) dd :: ["A"(0) x "A"(13)] -(13)-> "A"(13) dd :: ["A"(0) x "A"(6)] -(6)-> "A"(6) dd :: ["A"(0) x "A"(9)] -(9)-> "A"(9) flatten :: ["A"(13)] -(1)-> "A"(13) flatten'1 :: ["A"(13)] -(1)-> "A"(13) insert :: ["A"(0) x "A"(6)] -(6)-> "A"(6) insert'1 :: ["A"(6) x "A"(0)] -(6)-> "A"(6) insert'2 :: ["A"(1) x "A"(0) x "A"(0) x "A"(6)] -(12)-> "A"(6) insertionsort :: ["A"(13)] -(1)-> "A"(6) insertionsort'1 :: ["A"(13)] -(1)-> "A"(6) leaf :: [] -(0)-> "A"(13) nil :: [] -(0)-> "A"(13) nil :: [] -(0)-> "A"(6) nil :: [] -(0)-> "A"(15) node :: ["A"(13) x "A"(13) x "A"(13)] -(13)-> "A"(13) append# :: ["A"(9) x "A"(1)] -(12)-> "A"(1) append'1# :: ["A"(9) x "A"(1)] -(8)-> "A"(12) flatten# :: ["A"(13)] -(15)-> "A"(1) flatten'1# :: ["A"(13)] -(15)-> "A"(1) flattensort# :: ["A"(15)] -(13)-> "A"(0) insert# :: ["A"(0) x "A"(6)] -(3)-> "A"(0) insert'1# :: ["A"(6) x "A"(0)] -(0)-> "A"(12) insert'2# :: ["A"(1) x "A"(0) x "A"(0) x "A"(6)] -(5)-> "A"(9) insertionsort# :: ["A"(13)] -(2)-> "A"(0) insertionsort'1# :: ["A"(13)] -(0)-> "A"(0) c_17 :: ["A"(0)] -(0)-> "A"(12) c_18 :: ["A"(0)] -(0)-> "A"(15) c_24 :: ["A"(0)] -(0)-> "A"(15) c_25 :: ["A"(0)] -(0)-> "A"(15) c_28 :: ["A"(0)] -(0)-> "A"(11) Cost-free Signatures used: -------------------------- Base Constructor Signatures used: --------------------------------- "'0_A" :: [] -(0)-> "A"(1) "'EQ_A" :: [] -(0)-> "A"(1) "'GT_A" :: [] -(0)-> "A"(1) "'LT_A" :: [] -(0)-> "A"(1) "'false_A" :: [] -(0)-> "A"(1) "'neg_A" :: ["A"(0)] -(0)-> "A"(1) "'pos_A" :: ["A"(0)] -(1)-> "A"(1) "'s_A" :: ["A"(0)] -(1)-> "A"(1) "'true_A" :: [] -(0)-> "A"(1) "c_17_A" :: ["A"(0)] -(0)-> "A"(1) "c_18_A" :: ["A"(0)] -(0)-> "A"(1) "c_24_A" :: ["A"(0)] -(0)-> "A"(1) "c_25_A" :: ["A"(0)] -(0)-> "A"(1) "c_28_A" :: ["A"(0)] -(0)-> "A"(1) "dd_A" :: ["A"(0) x "A"(1)] -(1)-> "A"(1) "leaf_A" :: [] -(0)-> "A"(1) "nil_A" :: [] -(0)-> "A"(1) "node_A" :: ["A"(1) x "A"(1) x "A"(1)] -(1)-> "A"(1) Following Still Strict Rules were Typed as: ------------------------------------------- 1. Strict: insert#(x,l) -> c_24(insert'1#(l,x)) 2. Weak: *** Step 6.b:1.b:1: RemoveWeakSuffixes WORST_CASE(?,O(n^1)) + Considered Problem: - Strict DPs: 'compare#('neg(x),'neg(y)) -> c_9('compare#(y,x)) 'compare#('pos(x),'pos(y)) -> c_13('compare#(x,y)) 'compare#('s(x),'s(y)) -> c_15('compare#(x,y)) 'less#(x,y) -> c_16('compare#(x,y)) - Weak DPs: append#(l1,l2) -> append'1#(l1,l2) append'1#(dd(x,xs),l2) -> append#(xs,l2) flatten#(t) -> flatten'1#(t) flatten'1#(node(l,t1,t2)) -> append#(l,append(flatten(t1),flatten(t2))) flatten'1#(node(l,t1,t2)) -> append#(flatten(t1),flatten(t2)) flatten'1#(node(l,t1,t2)) -> flatten#(t1) flatten'1#(node(l,t1,t2)) -> flatten#(t2) flattensort#(t) -> flatten#(t) flattensort#(t) -> insertionsort#(flatten(t)) insert#(x,l) -> insert'1#(l,x) insert'1#(dd(y,ys),x) -> 'less#(y,x) insert'1#(dd(y,ys),x) -> insert'2#('less(y,x),x,y,ys) insert'2#('true(),x,y,ys) -> insert#(x,ys) insertionsort#(l) -> insertionsort'1#(l) insertionsort'1#(dd(x,xs)) -> insert#(x,insertionsort(xs)) insertionsort'1#(dd(x,xs)) -> insertionsort#(xs) - Weak TRS: 'cklt('EQ()) -> 'false() 'cklt('GT()) -> 'false() 'cklt('LT()) -> 'true() 'compare('0(),'0()) -> 'EQ() 'compare('0(),'neg(y)) -> 'GT() 'compare('0(),'pos(y)) -> 'LT() 'compare('0(),'s(y)) -> 'LT() 'compare('neg(x),'0()) -> 'LT() 'compare('neg(x),'neg(y)) -> 'compare(y,x) 'compare('neg(x),'pos(y)) -> 'LT() 'compare('pos(x),'0()) -> 'GT() 'compare('pos(x),'neg(y)) -> 'GT() 'compare('pos(x),'pos(y)) -> 'compare(x,y) 'compare('s(x),'0()) -> 'GT() 'compare('s(x),'s(y)) -> 'compare(x,y) 'less(x,y) -> 'cklt('compare(x,y)) append(l1,l2) -> append'1(l1,l2) append'1(dd(x,xs),l2) -> dd(x,append(xs,l2)) append'1(nil(),l2) -> l2 flatten(t) -> flatten'1(t) flatten'1(leaf()) -> nil() flatten'1(node(l,t1,t2)) -> append(l,append(flatten(t1),flatten(t2))) insert(x,l) -> insert'1(l,x) insert'1(dd(y,ys),x) -> insert'2('less(y,x),x,y,ys) insert'1(nil(),x) -> dd(x,nil()) insert'2('false(),x,y,ys) -> dd(x,dd(y,ys)) insert'2('true(),x,y,ys) -> dd(y,insert(x,ys)) insertionsort(l) -> insertionsort'1(l) insertionsort'1(dd(x,xs)) -> insert(x,insertionsort(xs)) insertionsort'1(nil()) -> nil() - Signature: {'cklt/1,'compare/2,'less/2,append/2,append'1/2,flatten/1,flatten'1/1,flattensort/1,insert/2,insert'1/2 ,insert'2/4,insertionsort/1,insertionsort'1/1,'cklt#/1,'compare#/2,'less#/2,append#/2,append'1#/2,flatten#/1 ,flatten'1#/1,flattensort#/1,insert#/2,insert'1#/2,insert'2#/4,insertionsort#/1,insertionsort'1#/1} / {'0/0 ,'EQ/0,'GT/0,'LT/0,'false/0,'neg/1,'pos/1,'s/1,'true/0,dd/2,leaf/0,nil/0,node/3,c_1/0,c_2/0,c_3/0,c_4/0 ,c_5/0,c_6/0,c_7/0,c_8/0,c_9/1,c_10/0,c_11/0,c_12/0,c_13/1,c_14/0,c_15/1,c_16/1,c_17/1,c_18/1,c_19/0,c_20/1 ,c_21/0,c_22/4,c_23/2,c_24/1,c_25/2,c_26/0,c_27/0,c_28/1,c_29/1,c_30/2,c_31/0} - Obligation: innermost runtime complexity wrt. defined symbols {'cklt#,'compare#,'less#,append#,append'1#,flatten# ,flatten'1#,flattensort#,insert#,insert'1#,insert'2#,insertionsort#,insertionsort'1#} and constructors {'0 ,'EQ,'GT,'LT,'false,'neg,'pos,'s,'true,dd,leaf,nil,node} + Applied Processor: RemoveWeakSuffixes + Details: Consider the dependency graph 1:S:'compare#('neg(x),'neg(y)) -> c_9('compare#(y,x)) -->_1 'compare#('s(x),'s(y)) -> c_15('compare#(x,y)):3 -->_1 'compare#('pos(x),'pos(y)) -> c_13('compare#(x,y)):2 -->_1 'compare#('neg(x),'neg(y)) -> c_9('compare#(y,x)):1 2:S:'compare#('pos(x),'pos(y)) -> c_13('compare#(x,y)) -->_1 'compare#('s(x),'s(y)) -> c_15('compare#(x,y)):3 -->_1 'compare#('pos(x),'pos(y)) -> c_13('compare#(x,y)):2 -->_1 'compare#('neg(x),'neg(y)) -> c_9('compare#(y,x)):1 3:S:'compare#('s(x),'s(y)) -> c_15('compare#(x,y)) -->_1 'compare#('s(x),'s(y)) -> c_15('compare#(x,y)):3 -->_1 'compare#('pos(x),'pos(y)) -> c_13('compare#(x,y)):2 -->_1 'compare#('neg(x),'neg(y)) -> c_9('compare#(y,x)):1 4:S:'less#(x,y) -> c_16('compare#(x,y)) -->_1 'compare#('s(x),'s(y)) -> c_15('compare#(x,y)):3 -->_1 'compare#('pos(x),'pos(y)) -> c_13('compare#(x,y)):2 -->_1 'compare#('neg(x),'neg(y)) -> c_9('compare#(y,x)):1 5:W:append#(l1,l2) -> append'1#(l1,l2) -->_1 append'1#(dd(x,xs),l2) -> append#(xs,l2):6 6:W:append'1#(dd(x,xs),l2) -> append#(xs,l2) -->_1 append#(l1,l2) -> append'1#(l1,l2):5 7:W:flatten#(t) -> flatten'1#(t) -->_1 flatten'1#(node(l,t1,t2)) -> flatten#(t2):11 -->_1 flatten'1#(node(l,t1,t2)) -> flatten#(t1):10 -->_1 flatten'1#(node(l,t1,t2)) -> append#(flatten(t1),flatten(t2)):9 -->_1 flatten'1#(node(l,t1,t2)) -> append#(l,append(flatten(t1),flatten(t2))):8 8:W:flatten'1#(node(l,t1,t2)) -> append#(l,append(flatten(t1),flatten(t2))) -->_1 append#(l1,l2) -> append'1#(l1,l2):5 9:W:flatten'1#(node(l,t1,t2)) -> append#(flatten(t1),flatten(t2)) -->_1 append#(l1,l2) -> append'1#(l1,l2):5 10:W:flatten'1#(node(l,t1,t2)) -> flatten#(t1) -->_1 flatten#(t) -> flatten'1#(t):7 11:W:flatten'1#(node(l,t1,t2)) -> flatten#(t2) -->_1 flatten#(t) -> flatten'1#(t):7 12:W:flattensort#(t) -> flatten#(t) -->_1 flatten#(t) -> flatten'1#(t):7 13:W:flattensort#(t) -> insertionsort#(flatten(t)) -->_1 insertionsort#(l) -> insertionsort'1#(l):18 14:W:insert#(x,l) -> insert'1#(l,x) -->_1 insert'1#(dd(y,ys),x) -> insert'2#('less(y,x),x,y,ys):16 -->_1 insert'1#(dd(y,ys),x) -> 'less#(y,x):15 15:W:insert'1#(dd(y,ys),x) -> 'less#(y,x) -->_1 'less#(x,y) -> c_16('compare#(x,y)):4 16:W:insert'1#(dd(y,ys),x) -> insert'2#('less(y,x),x,y,ys) -->_1 insert'2#('true(),x,y,ys) -> insert#(x,ys):17 17:W:insert'2#('true(),x,y,ys) -> insert#(x,ys) -->_1 insert#(x,l) -> insert'1#(l,x):14 18:W:insertionsort#(l) -> insertionsort'1#(l) -->_1 insertionsort'1#(dd(x,xs)) -> insertionsort#(xs):20 -->_1 insertionsort'1#(dd(x,xs)) -> insert#(x,insertionsort(xs)):19 19:W:insertionsort'1#(dd(x,xs)) -> insert#(x,insertionsort(xs)) -->_1 insert#(x,l) -> insert'1#(l,x):14 20:W:insertionsort'1#(dd(x,xs)) -> insertionsort#(xs) -->_1 insertionsort#(l) -> insertionsort'1#(l):18 The following weak DPs constitute a sub-graph of the DG that is closed under successors. The DPs are removed. 12: flattensort#(t) -> flatten#(t) 7: flatten#(t) -> flatten'1#(t) 11: flatten'1#(node(l,t1,t2)) -> flatten#(t2) 10: flatten'1#(node(l,t1,t2)) -> flatten#(t1) 8: flatten'1#(node(l,t1,t2)) -> append#(l,append(flatten(t1),flatten(t2))) 9: flatten'1#(node(l,t1,t2)) -> append#(flatten(t1),flatten(t2)) 5: append#(l1,l2) -> append'1#(l1,l2) 6: append'1#(dd(x,xs),l2) -> append#(xs,l2) *** Step 6.b:1.b:2: Ara WORST_CASE(?,O(n^1)) + Considered Problem: - Strict DPs: 'compare#('neg(x),'neg(y)) -> c_9('compare#(y,x)) 'compare#('pos(x),'pos(y)) -> c_13('compare#(x,y)) 'compare#('s(x),'s(y)) -> c_15('compare#(x,y)) 'less#(x,y) -> c_16('compare#(x,y)) - Weak DPs: flattensort#(t) -> insertionsort#(flatten(t)) insert#(x,l) -> insert'1#(l,x) insert'1#(dd(y,ys),x) -> 'less#(y,x) insert'1#(dd(y,ys),x) -> insert'2#('less(y,x),x,y,ys) insert'2#('true(),x,y,ys) -> insert#(x,ys) insertionsort#(l) -> insertionsort'1#(l) insertionsort'1#(dd(x,xs)) -> insert#(x,insertionsort(xs)) insertionsort'1#(dd(x,xs)) -> insertionsort#(xs) - Weak TRS: 'cklt('EQ()) -> 'false() 'cklt('GT()) -> 'false() 'cklt('LT()) -> 'true() 'compare('0(),'0()) -> 'EQ() 'compare('0(),'neg(y)) -> 'GT() 'compare('0(),'pos(y)) -> 'LT() 'compare('0(),'s(y)) -> 'LT() 'compare('neg(x),'0()) -> 'LT() 'compare('neg(x),'neg(y)) -> 'compare(y,x) 'compare('neg(x),'pos(y)) -> 'LT() 'compare('pos(x),'0()) -> 'GT() 'compare('pos(x),'neg(y)) -> 'GT() 'compare('pos(x),'pos(y)) -> 'compare(x,y) 'compare('s(x),'0()) -> 'GT() 'compare('s(x),'s(y)) -> 'compare(x,y) 'less(x,y) -> 'cklt('compare(x,y)) append(l1,l2) -> append'1(l1,l2) append'1(dd(x,xs),l2) -> dd(x,append(xs,l2)) append'1(nil(),l2) -> l2 flatten(t) -> flatten'1(t) flatten'1(leaf()) -> nil() flatten'1(node(l,t1,t2)) -> append(l,append(flatten(t1),flatten(t2))) insert(x,l) -> insert'1(l,x) insert'1(dd(y,ys),x) -> insert'2('less(y,x),x,y,ys) insert'1(nil(),x) -> dd(x,nil()) insert'2('false(),x,y,ys) -> dd(x,dd(y,ys)) insert'2('true(),x,y,ys) -> dd(y,insert(x,ys)) insertionsort(l) -> insertionsort'1(l) insertionsort'1(dd(x,xs)) -> insert(x,insertionsort(xs)) insertionsort'1(nil()) -> nil() - Signature: {'cklt/1,'compare/2,'less/2,append/2,append'1/2,flatten/1,flatten'1/1,flattensort/1,insert/2,insert'1/2 ,insert'2/4,insertionsort/1,insertionsort'1/1,'cklt#/1,'compare#/2,'less#/2,append#/2,append'1#/2,flatten#/1 ,flatten'1#/1,flattensort#/1,insert#/2,insert'1#/2,insert'2#/4,insertionsort#/1,insertionsort'1#/1} / {'0/0 ,'EQ/0,'GT/0,'LT/0,'false/0,'neg/1,'pos/1,'s/1,'true/0,dd/2,leaf/0,nil/0,node/3,c_1/0,c_2/0,c_3/0,c_4/0 ,c_5/0,c_6/0,c_7/0,c_8/0,c_9/1,c_10/0,c_11/0,c_12/0,c_13/1,c_14/0,c_15/1,c_16/1,c_17/1,c_18/1,c_19/0,c_20/1 ,c_21/0,c_22/4,c_23/2,c_24/1,c_25/2,c_26/0,c_27/0,c_28/1,c_29/1,c_30/2,c_31/0} - Obligation: innermost runtime complexity wrt. defined symbols {'cklt#,'compare#,'less#,append#,append'1#,flatten# ,flatten'1#,flattensort#,insert#,insert'1#,insert'2#,insertionsort#,insertionsort'1#} and constructors {'0 ,'EQ,'GT,'LT,'false,'neg,'pos,'s,'true,dd,leaf,nil,node} + Applied Processor: Ara {araHeuristics = NoHeuristics, minDegree = 1, maxDegree = 2, araTimeout = 8, araRuleShifting = Just 1} + Details: Signatures used: ---------------- '0 :: [] -(0)-> "A"(0) 'EQ :: [] -(0)-> "A"(0) 'GT :: [] -(0)-> "A"(0) 'LT :: [] -(0)-> "A"(0) 'cklt :: ["A"(0)] -(0)-> "A"(0) 'compare :: ["A"(0) x "A"(0)] -(0)-> "A"(0) 'false :: [] -(0)-> "A"(0) 'less :: ["A"(0) x "A"(0)] -(0)-> "A"(0) 'neg :: ["A"(0)] -(0)-> "A"(0) 'pos :: ["A"(0)] -(0)-> "A"(0) 's :: ["A"(0)] -(0)-> "A"(0) 'true :: [] -(0)-> "A"(0) append :: ["A"(0) x "A"(0)] -(0)-> "A"(0) append'1 :: ["A"(0) x "A"(0)] -(0)-> "A"(0) dd :: ["A"(0) x "A"(0)] -(0)-> "A"(0) flatten :: ["A"(0)] -(0)-> "A"(0) flatten'1 :: ["A"(0)] -(0)-> "A"(0) insert :: ["A"(0) x "A"(0)] -(0)-> "A"(0) insert'1 :: ["A"(0) x "A"(0)] -(0)-> "A"(0) insert'2 :: ["A"(0) x "A"(0) x "A"(0) x "A"(0)] -(0)-> "A"(0) insertionsort :: ["A"(0)] -(0)-> "A"(0) insertionsort'1 :: ["A"(0)] -(0)-> "A"(0) leaf :: [] -(0)-> "A"(0) nil :: [] -(0)-> "A"(0) node :: ["A"(0) x "A"(0) x "A"(0)] -(0)-> "A"(0) 'compare# :: ["A"(0) x "A"(0)] -(0)-> "A"(0) 'less# :: ["A"(0) x "A"(0)] -(1)-> "A"(0) flattensort# :: ["A"(0)] -(1)-> "A"(0) insert# :: ["A"(0) x "A"(0)] -(1)-> "A"(0) insert'1# :: ["A"(0) x "A"(0)] -(1)-> "A"(0) insert'2# :: ["A"(0) x "A"(0) x "A"(0) x "A"(0)] -(1)-> "A"(0) insertionsort# :: ["A"(0)] -(1)-> "A"(0) insertionsort'1# :: ["A"(0)] -(1)-> "A"(0) c_9 :: ["A"(0)] -(0)-> "A"(0) c_13 :: ["A"(0)] -(0)-> "A"(0) c_15 :: ["A"(0)] -(0)-> "A"(0) c_16 :: ["A"(0)] -(0)-> "A"(0) Cost-free Signatures used: -------------------------- Base Constructor Signatures used: --------------------------------- Following Still Strict Rules were Typed as: ------------------------------------------- 1. Strict: 'less#(x,y) -> c_16('compare#(x,y)) 2. Weak: 'compare#('neg(x),'neg(y)) -> c_9('compare#(y,x)) 'compare#('pos(x),'pos(y)) -> c_13('compare#(x,y)) 'compare#('s(x),'s(y)) -> c_15('compare#(x,y)) *** Step 6.b:1.b:3: Ara WORST_CASE(?,O(n^1)) + Considered Problem: - Strict DPs: 'compare#('neg(x),'neg(y)) -> c_9('compare#(y,x)) 'compare#('pos(x),'pos(y)) -> c_13('compare#(x,y)) 'compare#('s(x),'s(y)) -> c_15('compare#(x,y)) - Weak DPs: 'less#(x,y) -> c_16('compare#(x,y)) flattensort#(t) -> insertionsort#(flatten(t)) insert#(x,l) -> insert'1#(l,x) insert'1#(dd(y,ys),x) -> 'less#(y,x) insert'1#(dd(y,ys),x) -> insert'2#('less(y,x),x,y,ys) insert'2#('true(),x,y,ys) -> insert#(x,ys) insertionsort#(l) -> insertionsort'1#(l) insertionsort'1#(dd(x,xs)) -> insert#(x,insertionsort(xs)) insertionsort'1#(dd(x,xs)) -> insertionsort#(xs) - Weak TRS: 'cklt('EQ()) -> 'false() 'cklt('GT()) -> 'false() 'cklt('LT()) -> 'true() 'compare('0(),'0()) -> 'EQ() 'compare('0(),'neg(y)) -> 'GT() 'compare('0(),'pos(y)) -> 'LT() 'compare('0(),'s(y)) -> 'LT() 'compare('neg(x),'0()) -> 'LT() 'compare('neg(x),'neg(y)) -> 'compare(y,x) 'compare('neg(x),'pos(y)) -> 'LT() 'compare('pos(x),'0()) -> 'GT() 'compare('pos(x),'neg(y)) -> 'GT() 'compare('pos(x),'pos(y)) -> 'compare(x,y) 'compare('s(x),'0()) -> 'GT() 'compare('s(x),'s(y)) -> 'compare(x,y) 'less(x,y) -> 'cklt('compare(x,y)) append(l1,l2) -> append'1(l1,l2) append'1(dd(x,xs),l2) -> dd(x,append(xs,l2)) append'1(nil(),l2) -> l2 flatten(t) -> flatten'1(t) flatten'1(leaf()) -> nil() flatten'1(node(l,t1,t2)) -> append(l,append(flatten(t1),flatten(t2))) insert(x,l) -> insert'1(l,x) insert'1(dd(y,ys),x) -> insert'2('less(y,x),x,y,ys) insert'1(nil(),x) -> dd(x,nil()) insert'2('false(),x,y,ys) -> dd(x,dd(y,ys)) insert'2('true(),x,y,ys) -> dd(y,insert(x,ys)) insertionsort(l) -> insertionsort'1(l) insertionsort'1(dd(x,xs)) -> insert(x,insertionsort(xs)) insertionsort'1(nil()) -> nil() - Signature: {'cklt/1,'compare/2,'less/2,append/2,append'1/2,flatten/1,flatten'1/1,flattensort/1,insert/2,insert'1/2 ,insert'2/4,insertionsort/1,insertionsort'1/1,'cklt#/1,'compare#/2,'less#/2,append#/2,append'1#/2,flatten#/1 ,flatten'1#/1,flattensort#/1,insert#/2,insert'1#/2,insert'2#/4,insertionsort#/1,insertionsort'1#/1} / {'0/0 ,'EQ/0,'GT/0,'LT/0,'false/0,'neg/1,'pos/1,'s/1,'true/0,dd/2,leaf/0,nil/0,node/3,c_1/0,c_2/0,c_3/0,c_4/0 ,c_5/0,c_6/0,c_7/0,c_8/0,c_9/1,c_10/0,c_11/0,c_12/0,c_13/1,c_14/0,c_15/1,c_16/1,c_17/1,c_18/1,c_19/0,c_20/1 ,c_21/0,c_22/4,c_23/2,c_24/1,c_25/2,c_26/0,c_27/0,c_28/1,c_29/1,c_30/2,c_31/0} - Obligation: innermost runtime complexity wrt. defined symbols {'cklt#,'compare#,'less#,append#,append'1#,flatten# ,flatten'1#,flattensort#,insert#,insert'1#,insert'2#,insertionsort#,insertionsort'1#} and constructors {'0 ,'EQ,'GT,'LT,'false,'neg,'pos,'s,'true,dd,leaf,nil,node} + Applied Processor: Ara {araHeuristics = NoHeuristics, minDegree = 1, maxDegree = 2, araTimeout = 8, araRuleShifting = Just 1} + Details: Signatures used: ---------------- '0 :: [] -(0)-> "A"(0) 'EQ :: [] -(0)-> "A"(0) 'EQ :: [] -(0)-> "A"(15) 'GT :: [] -(0)-> "A"(0) 'GT :: [] -(0)-> "A"(15) 'LT :: [] -(0)-> "A"(0) 'LT :: [] -(0)-> "A"(15) 'cklt :: ["A"(0)] -(0)-> "A"(15) 'compare :: ["A"(0) x "A"(0)] -(0)-> "A"(9) 'false :: [] -(0)-> "A"(1) 'false :: [] -(0)-> "A"(15) 'less :: ["A"(0) x "A"(0)] -(0)-> "A"(14) 'neg :: ["A"(8)] -(8)-> "A"(8) 'neg :: ["A"(0)] -(0)-> "A"(0) 'pos :: ["A"(8)] -(8)-> "A"(8) 'pos :: ["A"(0)] -(0)-> "A"(0) 's :: ["A"(8)] -(8)-> "A"(8) 's :: ["A"(0)] -(0)-> "A"(0) 'true :: [] -(0)-> "A"(1) 'true :: [] -(0)-> "A"(15) append :: ["A"(13) x "A"(13)] -(0)-> "A"(13) append'1 :: ["A"(13) x "A"(13)] -(0)-> "A"(13) dd :: ["A"(13) x "A"(13)] -(0)-> "A"(13) dd :: ["A"(8) x "A"(8)] -(0)-> "A"(8) dd :: ["A"(10) x "A"(10)] -(0)-> "A"(10) dd :: ["A"(11) x "A"(11)] -(0)-> "A"(11) flatten :: ["A"(15)] -(1)-> "A"(13) flatten'1 :: ["A"(15)] -(0)-> "A"(13) insert :: ["A"(8) x "A"(8)] -(0)-> "A"(8) insert'1 :: ["A"(8) x "A"(8)] -(0)-> "A"(8) insert'2 :: ["A"(1) x "A"(8) x "A"(8) x "A"(8)] -(0)-> "A"(8) insertionsort :: ["A"(10)] -(0)-> "A"(8) insertionsort'1 :: ["A"(10)] -(0)-> "A"(8) leaf :: [] -(0)-> "A"(15) nil :: [] -(0)-> "A"(13) nil :: [] -(0)-> "A"(8) nil :: [] -(0)-> "A"(10) nil :: [] -(0)-> "A"(15) node :: ["A"(15) x "A"(15) x "A"(15)] -(15)-> "A"(15) 'compare# :: ["A"(8) x "A"(8)] -(4)-> "A"(1) 'less# :: ["A"(8) x "A"(10)] -(14)-> "A"(9) flattensort# :: ["A"(15)] -(15)-> "A"(0) insert# :: ["A"(10) x "A"(8)] -(14)-> "A"(6) insert'1# :: ["A"(8) x "A"(10)] -(14)-> "A"(6) insert'2# :: ["A"(1) x "A"(10) x "A"(1) x "A"(8)] -(14)-> "A"(6) insertionsort# :: ["A"(11)] -(14)-> "A"(0) insertionsort'1# :: ["A"(11)] -(14)-> "A"(0) c_9 :: ["A"(0)] -(0)-> "A"(15) c_13 :: ["A"(0)] -(0)-> "A"(15) c_15 :: ["A"(0)] -(0)-> "A"(12) c_16 :: ["A"(0)] -(0)-> "A"(12) Cost-free Signatures used: -------------------------- Base Constructor Signatures used: --------------------------------- "'0_A" :: [] -(0)-> "A"(1) "'EQ_A" :: [] -(0)-> "A"(1) "'GT_A" :: [] -(0)-> "A"(1) "'LT_A" :: [] -(0)-> "A"(1) "'false_A" :: [] -(0)-> "A"(1) "'neg_A" :: ["A"(1)] -(1)-> "A"(1) "'pos_A" :: ["A"(1)] -(1)-> "A"(1) "'s_A" :: ["A"(1)] -(1)-> "A"(1) "'true_A" :: [] -(0)-> "A"(1) "c_13_A" :: ["A"(0)] -(0)-> "A"(1) "c_15_A" :: ["A"(0)] -(0)-> "A"(1) "c_16_A" :: ["A"(0)] -(0)-> "A"(1) "c_9_A" :: ["A"(0)] -(0)-> "A"(1) "dd_A" :: ["A"(1) x "A"(1)] -(0)-> "A"(1) "leaf_A" :: [] -(0)-> "A"(1) "nil_A" :: [] -(0)-> "A"(1) "node_A" :: ["A"(1) x "A"(1) x "A"(1)] -(1)-> "A"(1) Following Still Strict Rules were Typed as: ------------------------------------------- 1. Strict: 'compare#('neg(x),'neg(y)) -> c_9('compare#(y,x)) 'compare#('pos(x),'pos(y)) -> c_13('compare#(x,y)) 'compare#('s(x),'s(y)) -> c_15('compare#(x,y)) 2. Weak: WORST_CASE(?,O(n^3))